FS004N · theorem body

four_square_signed_conjugate_negative_blocks

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

When all four centered coordinate orientations are negative, every exact conjugate-quaternion positive/negative block is congruent modulo the multiplier.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Statement with defined notation

∀ k. ∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ModEq(k,e · e + f · f + g · g + h · h,0) → ModEq(k,a + e,0) → ModEq(k,b + f,0) → ModEq(k,c + g,0) → ModEq(k,d + h,0) → ModEq(k,a · e + b · f + c · g + d · h,0) ∧ (ModEq(k,a · f + c · h,b · e + d · g) ∧ (ModEq(k,a · g + d · f,c · e + b · h) ∧ ModEq(k,a · h + b · g,d · e + c · f)))

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq

In local proof propositions

PD0008 ModEq
Exact expanded first-order statement
forall k a b c d e f g h. (exists ftcn_left_fssbn_conjugate_negative_norm ftcn_right_fssbn_conjugate_negative_norm. (e * e + f * f + g * g + h * h) + (k) * ftcn_left_fssbn_conjugate_negative_norm = (0) + (k) * ftcn_right_fssbn_conjugate_negative_norm) -> (exists ftcn_left_fssbn_conjugate_negative_a_negative ftcn_right_fssbn_conjugate_negative_a_negative. (a + e) + (k) * ftcn_left_fssbn_conjugate_negative_a_negative = (0) + (k) * ftcn_right_fssbn_conjugate_negative_a_negative) -> (exists ftcn_left_fssbn_conjugate_negative_b_negative ftcn_right_fssbn_conjugate_negative_b_negative. (b + f) + (k) * ftcn_left_fssbn_conjugate_negative_b_negative = (0) + (k) * ftcn_right_fssbn_conjugate_negative_b_negative) -> (exists ftcn_left_fssbn_conjugate_negative_c_negative ftcn_right_fssbn_conjugate_negative_c_negative. (c + g) + (k) * ftcn_left_fssbn_conjugate_negative_c_negative = (0) + (k) * ftcn_right_fssbn_conjugate_negative_c_negative) -> (exists ftcn_left_fssbn_conjugate_negative_d_negative ftcn_right_fssbn_conjugate_negative_d_negative. (d + h) + (k) * ftcn_left_fssbn_conjugate_negative_d_negative = (0) + (k) * ftcn_right_fssbn_conjugate_negative_d_negative) -> ((exists ftcn_left_fssbn_conjugate_negative_block_0 ftcn_right_fssbn_conjugate_negative_block_0. (a * e + b * f + c * g + d * h) + (k) * ftcn_left_fssbn_conjugate_negative_block_0 = (0) + (k) * ftcn_right_fssbn_conjugate_negative_block_0) /\ ((exists ftcn_left_fssbn_conjugate_negative_block_1 ftcn_right_fssbn_conjugate_negative_block_1. (a * f + c * h) + (k) * ftcn_left_fssbn_conjugate_negative_block_1 = (b * e + d * g) + (k) * ftcn_right_fssbn_conjugate_negative_block_1) /\ ((exists ftcn_left_fssbn_conjugate_negative_block_2 ftcn_right_fssbn_conjugate_negative_block_2. (a * g + d * f) + (k) * ftcn_left_fssbn_conjugate_negative_block_2 = (c * e + b * h) + (k) * ftcn_right_fssbn_conjugate_negative_block_2) /\ (exists ftcn_left_fssbn_conjugate_negative_block_3 ftcn_right_fssbn_conjugate_negative_block_3. (a * h + b * g) + (k) * ftcn_left_fssbn_conjugate_negative_block_3 = (d * e + c * f) + (k) * ftcn_right_fssbn_conjugate_negative_block_3))))

Proof neighborhood

Direct theorem prerequisites

FS005V four_square_signed_dot_negative_zero FS005P four_square_signed_mod_zero_add FS002D four_square_euler_four_add_shuffle add_assoc · Stable closed FS005S four_square_signed_zero_cancel_right FS005N four_square_signed_cross_negative mod_eq_add · Stable closed

Direct theorem dependents

FS0055 four_square_signed_orientation_mask_15

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

155 script commands · 23 reading checkpoints · 14 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (5)
four square signed dot negative zerofour square signed mod zero addfour square euler four add shufflefour square signed zero cancel rightfour square signed cross negative
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro k
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro c
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro f
  8. L8
    intro g
  9. L9
    intro h
  10. L10
    intro hnorm
02Fix variables and assumptionsL11–14

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro ha
  2. L12
    intro hb
  3. L13
    intro hc
  4. L14
    intro hd
03Separate the logical casesL15–15

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L15
    split
04Establish hdaL16–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed dot negative zero.

  1. L16
    have hda : ModEq(k,a · e + e · e,0)Definitions: ModEq(k,a · e + e · e,0)Original native command in the exact edition
  2. L17
    specialize four_square_signed_dot_negative_zero k
  3. L18
    specialize four_square_signed_dot_negative_zero a
  4. L19
    specialize four_square_signed_dot_negative_zero e
  5. L20
    apply four_square_signed_dot_negative_zero
  6. L21
    exact ha
05Establish hdbL22–27

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed dot negative zero.

  1. L22
    have hdb : ModEq(k,b · f + f · f,0)Definitions: ModEq(k,b · f + f · f,0)Original native command in the exact edition
  2. L23
    specialize four_square_signed_dot_negative_zero k
  3. L24
    specialize four_square_signed_dot_negative_zero b
  4. L25
    specialize four_square_signed_dot_negative_zero f
  5. L26
    apply four_square_signed_dot_negative_zero
  6. L27
    exact hb
06Establish hdcL28–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed dot negative zero.

  1. L28
    have hdc : ModEq(k,c · g + g · g,0)Definitions: ModEq(k,c · g + g · g,0)Original native command in the exact edition
  2. L29
    specialize four_square_signed_dot_negative_zero k
  3. L30
    specialize four_square_signed_dot_negative_zero c
  4. L31
    specialize four_square_signed_dot_negative_zero g
  5. L32
    apply four_square_signed_dot_negative_zero
  6. L33
    exact hc
07Establish hddL34–39

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed dot negative zero.

  1. L34
    have hdd : ModEq(k,d · h + h · h,0)Definitions: ModEq(k,d · h + h · h,0)Original native command in the exact edition
  2. L35
    specialize four_square_signed_dot_negative_zero k
  3. L36
    specialize four_square_signed_dot_negative_zero d
  4. L37
    specialize four_square_signed_dot_negative_zero h
  5. L38
    apply four_square_signed_dot_negative_zero
  6. L39
    exact hd
08Establish habzeroL40–46

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed mod zero add.

  1. L40
    have habzero : ModEq(k,a · e + e · e + (b · f + f · f),0)Definitions: ModEq(k,a · e + e · e + (b · f + f · f),0)Original native command in the exact edition
  2. L41
    specialize four_square_signed_mod_zero_add k
  3. L42
    specialize four_square_signed_mod_zero_add (a * e + e * e)
  4. L43
    specialize four_square_signed_mod_zero_add (b * f + f * f)
  5. L44
    apply four_square_signed_mod_zero_add
  6. L45
    exact hda
  7. L46
    exact hdb
09Establish hcdzeroL47–53

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed mod zero add.

  1. L47
    have hcdzero : ModEq(k,c · g + g · g + (d · h + h · h),0)Definitions: ModEq(k,c · g + g · g + (d · h + h · h),0)Original native command in the exact edition
  2. L48
    specialize four_square_signed_mod_zero_add k
  3. L49
    specialize four_square_signed_mod_zero_add (c * g + g * g)
  4. L50
    specialize four_square_signed_mod_zero_add (d * h + h * h)
  5. L51
    apply four_square_signed_mod_zero_add
  6. L52
    exact hdc
  7. L53
    exact hdd
10Establish hallzeroL54–60

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed mod zero add.

  1. L54
    have hallzero : ModEq(k,a · e + e · e + (b · f + f · f) + (c · g + g · g + (d · h + h · h)),0)Definitions: ModEq(k,a · e + e · e + (b · f + f · f) + (c · g + g · g + (d · h + h · h)),0)Original native command in the exact edition
  2. L55
    specialize four_square_signed_mod_zero_add k
  3. L56
    specialize four_square_signed_mod_zero_add ((a * e + e * e) + (b * f + f * f))
  4. L57
    specialize four_square_signed_mod_zero_add ((c * g + g * g) + (d * h + h * h))
  5. L58
    apply four_square_signed_mod_zero_add
  6. L59
    exact habzero
  7. L60
    exact hcdzero
11Establish hshuffleL61–70

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square euler four add shuffle.

  1. L61
    have hshuffle : (((a * e + e * e) + (b * f + f * f)) + ((c * g + g * g) + (d * h + h * h))) = ((a * e + b * f + c * g + d * h) + (e * e + f * f + g * g + h * h))
  2. L62
    trans ((a * e + b * f) + (c * g + d * h)) + ((e * e + f * f) + (g * g + h * h))
  3. L63
    apply four_square_euler_four_add_shuffle
  4. L64
    congr
  5. L65
    symm
  6. L66
    apply add_assoc
  7. L67
    symm
  8. L68
    apply add_assoc
  9. L69
    rewrite hshuffle at hallzero
  10. L70
    specialize four_square_signed_zero_cancel_right k
12Use earlier factsL71–75

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L71
    specialize four_square_signed_zero_cancel_right (a * e + b * f + c * g + d * h)
  2. L72
    specialize four_square_signed_zero_cancel_right (e * e + f * f + g * g + h * h)
  3. L73
    apply four_square_signed_zero_cancel_right
  4. L74
    exact hallzero
  5. L75
    exact hnorm
13Separate the logical casesL76–76

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L76
    split
14Establish hnegative_one_firstL77–85

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cross negative.

  1. L77
    have hnegative_one_first : ModEq(k,a · f,b · e)Definitions: ModEq(k,a · f,b · e)Original native command in the exact edition
  2. L78
    specialize four_square_signed_cross_negative k
  3. L79
    specialize four_square_signed_cross_negative a
  4. L80
    specialize four_square_signed_cross_negative b
  5. L81
    specialize four_square_signed_cross_negative e
  6. L82
    specialize four_square_signed_cross_negative f
  7. L83
    apply four_square_signed_cross_negative
  8. L84
    exact ha
  9. L85
    exact hb
15Establish hnegative_one_secondL86–95

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cross negative.

  1. L86
    have hnegative_one_second : ModEq(k,c · h,d · g)Definitions: ModEq(k,c · h,d · g)Original native command in the exact edition
  2. L87
    specialize four_square_signed_cross_negative k
  3. L88
    specialize four_square_signed_cross_negative c
  4. L89
    specialize four_square_signed_cross_negative d
  5. L90
    specialize four_square_signed_cross_negative g
  6. L91
    specialize four_square_signed_cross_negative h
  7. L92
    apply four_square_signed_cross_negative
  8. L93
    exact hc
  9. L94
    exact hd
  10. L95
    specialize mod_eq_add k
16Use earlier factsL96–102

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L96
    specialize mod_eq_add (a * f)
  2. L97
    specialize mod_eq_add (b * e)
  3. L98
    specialize mod_eq_add (c * h)
  4. L99
    specialize mod_eq_add (d * g)
  5. L100
    apply mod_eq_add
  6. L101
    exact hnegative_one_first
  7. L102
    exact hnegative_one_second
17Separate the logical casesL103–103

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L103
    split
18Establish hnegative_two_firstL104–112

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cross negative.

  1. L104
    have hnegative_two_first : ModEq(k,a · g,c · e)Definitions: ModEq(k,a · g,c · e)Original native command in the exact edition
  2. L105
    specialize four_square_signed_cross_negative k
  3. L106
    specialize four_square_signed_cross_negative a
  4. L107
    specialize four_square_signed_cross_negative c
  5. L108
    specialize four_square_signed_cross_negative e
  6. L109
    specialize four_square_signed_cross_negative g
  7. L110
    apply four_square_signed_cross_negative
  8. L111
    exact ha
  9. L112
    exact hc
19Establish hnegative_two_secondL113–122

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cross negative.

  1. L113
    have hnegative_two_second : ModEq(k,d · f,b · h)Definitions: ModEq(k,d · f,b · h)Original native command in the exact edition
  2. L114
    specialize four_square_signed_cross_negative k
  3. L115
    specialize four_square_signed_cross_negative d
  4. L116
    specialize four_square_signed_cross_negative b
  5. L117
    specialize four_square_signed_cross_negative h
  6. L118
    specialize four_square_signed_cross_negative f
  7. L119
    apply four_square_signed_cross_negative
  8. L120
    exact hd
  9. L121
    exact hb
  10. L122
    specialize mod_eq_add k
20Use earlier factsL123–129

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L123
    specialize mod_eq_add (a * g)
  2. L124
    specialize mod_eq_add (c * e)
  3. L125
    specialize mod_eq_add (d * f)
  4. L126
    specialize mod_eq_add (b * h)
  5. L127
    apply mod_eq_add
  6. L128
    exact hnegative_two_first
  7. L129
    exact hnegative_two_second
21Establish hnegative_three_firstL130–138

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cross negative.

  1. L130
    have hnegative_three_first : ModEq(k,a · h,d · e)Definitions: ModEq(k,a · h,d · e)Original native command in the exact edition
  2. L131
    specialize four_square_signed_cross_negative k
  3. L132
    specialize four_square_signed_cross_negative a
  4. L133
    specialize four_square_signed_cross_negative d
  5. L134
    specialize four_square_signed_cross_negative e
  6. L135
    specialize four_square_signed_cross_negative h
  7. L136
    apply four_square_signed_cross_negative
  8. L137
    exact ha
  9. L138
    exact hd
22Establish hnegative_three_secondL139–148

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply four square signed cross negative.

  1. L139
    have hnegative_three_second : ModEq(k,b · g,c · f)Definitions: ModEq(k,b · g,c · f)Original native command in the exact edition
  2. L140
    specialize four_square_signed_cross_negative k
  3. L141
    specialize four_square_signed_cross_negative b
  4. L142
    specialize four_square_signed_cross_negative c
  5. L143
    specialize four_square_signed_cross_negative f
  6. L144
    specialize four_square_signed_cross_negative g
  7. L145
    apply four_square_signed_cross_negative
  8. L146
    exact hb
  9. L147
    exact hc
  10. L148
    specialize mod_eq_add k
23Use earlier factsL149–155

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L149
    specialize mod_eq_add (a * h)
  2. L150
    specialize mod_eq_add (d * e)
  3. L151
    specialize mod_eq_add (b * g)
  4. L152
    specialize mod_eq_add (c * f)
  5. L153
    apply mod_eq_add
  6. L154
    exact hnegative_three_first
  7. L155
    exact hnegative_three_second

Library-wide reading audit

Original defined command ledger · 155 lines
  1. 0001intro k
  2. 0002intro a
  3. 0003intro b
  4. 0004intro c
  5. 0005intro d
  6. 0006intro e
  7. 0007intro f
  8. 0008intro g
  9. 0009intro h
  10. 0010intro hnorm
  11. 0011intro ha
  12. 0012intro hb
  13. 0013intro hc
  14. 0014intro hd
  15. 0015split
  16. 0016have hda : ModEq(k,a · e + e · e,0)
    Exact native replay linehave hda : exists ftcn_left_fssbn_hda ftcn_right_fssbn_hda. (a * e + e * e) + (k) * ftcn_left_fssbn_hda = (0) + (k) * ftcn_right_fssbn_hda
  17. 0017specialize four_square_signed_dot_negative_zero k
  18. 0018specialize four_square_signed_dot_negative_zero a
  19. 0019specialize four_square_signed_dot_negative_zero e
  20. 0020apply four_square_signed_dot_negative_zero
  21. 0021exact ha
  22. 0022have hdb : ModEq(k,b · f + f · f,0)
    Exact native replay linehave hdb : exists ftcn_left_fssbn_hdb ftcn_right_fssbn_hdb. (b * f + f * f) + (k) * ftcn_left_fssbn_hdb = (0) + (k) * ftcn_right_fssbn_hdb
  23. 0023specialize four_square_signed_dot_negative_zero k
  24. 0024specialize four_square_signed_dot_negative_zero b
  25. 0025specialize four_square_signed_dot_negative_zero f
  26. 0026apply four_square_signed_dot_negative_zero
  27. 0027exact hb
  28. 0028have hdc : ModEq(k,c · g + g · g,0)
    Exact native replay linehave hdc : exists ftcn_left_fssbn_hdc ftcn_right_fssbn_hdc. (c * g + g * g) + (k) * ftcn_left_fssbn_hdc = (0) + (k) * ftcn_right_fssbn_hdc
  29. 0029specialize four_square_signed_dot_negative_zero k
  30. 0030specialize four_square_signed_dot_negative_zero c
  31. 0031specialize four_square_signed_dot_negative_zero g
  32. 0032apply four_square_signed_dot_negative_zero
  33. 0033exact hc
  34. 0034have hdd : ModEq(k,d · h + h · h,0)
    Exact native replay linehave hdd : exists ftcn_left_fssbn_hdd ftcn_right_fssbn_hdd. (d * h + h * h) + (k) * ftcn_left_fssbn_hdd = (0) + (k) * ftcn_right_fssbn_hdd
  35. 0035specialize four_square_signed_dot_negative_zero k
  36. 0036specialize four_square_signed_dot_negative_zero d
  37. 0037specialize four_square_signed_dot_negative_zero h
  38. 0038apply four_square_signed_dot_negative_zero
  39. 0039exact hd
  40. 0040have habzero : ModEq(k,a · e + e · e + (b · f + f · f),0)
    Exact native replay linehave habzero : exists ftcn_left_fssbn_habzero ftcn_right_fssbn_habzero. ((a * e + e * e) + (b * f + f * f)) + (k) * ftcn_left_fssbn_habzero = (0) + (k) * ftcn_right_fssbn_habzero
  41. 0041specialize four_square_signed_mod_zero_add k
  42. 0042specialize four_square_signed_mod_zero_add (a * e + e * e)
  43. 0043specialize four_square_signed_mod_zero_add (b * f + f * f)
  44. 0044apply four_square_signed_mod_zero_add
  45. 0045exact hda
  46. 0046exact hdb
  47. 0047have hcdzero : ModEq(k,c · g + g · g + (d · h + h · h),0)
    Exact native replay linehave hcdzero : exists ftcn_left_fssbn_hcdzero ftcn_right_fssbn_hcdzero. ((c * g + g * g) + (d * h + h * h)) + (k) * ftcn_left_fssbn_hcdzero = (0) + (k) * ftcn_right_fssbn_hcdzero
  48. 0048specialize four_square_signed_mod_zero_add k
  49. 0049specialize four_square_signed_mod_zero_add (c * g + g * g)
  50. 0050specialize four_square_signed_mod_zero_add (d * h + h * h)
  51. 0051apply four_square_signed_mod_zero_add
  52. 0052exact hdc
  53. 0053exact hdd
  54. 0054have hallzero : ModEq(k,a · e + e · e + (b · f + f · f) + (c · g + g · g + (d · h + h · h)),0)
    Exact native replay linehave hallzero : exists ftcn_left_fssbn_hallzero ftcn_right_fssbn_hallzero. (((a * e + e * e) + (b * f + f * f)) + ((c * g + g * g) + (d * h + h * h))) + (k) * ftcn_left_fssbn_hallzero = (0) + (k) * ftcn_right_fssbn_hallzero
  55. 0055specialize four_square_signed_mod_zero_add k
  56. 0056specialize four_square_signed_mod_zero_add ((a * e + e * e) + (b * f + f * f))
  57. 0057specialize four_square_signed_mod_zero_add ((c * g + g * g) + (d * h + h * h))
  58. 0058apply four_square_signed_mod_zero_add
  59. 0059exact habzero
  60. 0060exact hcdzero
  61. 0061have hshuffle : (((a * e + e * e) + (b * f + f * f)) + ((c * g + g * g) + (d * h + h * h))) = ((a * e + b * f + c * g + d * h) + (e * e + f * f + g * g + h * h))
  62. 0062trans ((a * e + b * f) + (c * g + d * h)) + ((e * e + f * f) + (g * g + h * h))
  63. 0063apply four_square_euler_four_add_shuffle
  64. 0064congr
  65. 0065symm
  66. 0066apply add_assoc
  67. 0067symm
  68. 0068apply add_assoc
  69. 0069rewrite hshuffle at hallzero
  70. 0070specialize four_square_signed_zero_cancel_right k
  71. 0071specialize four_square_signed_zero_cancel_right (a * e + b * f + c * g + d * h)
  72. 0072specialize four_square_signed_zero_cancel_right (e * e + f * f + g * g + h * h)
  73. 0073apply four_square_signed_zero_cancel_right
  74. 0074exact hallzero
  75. 0075exact hnorm
  76. 0076split
  77. 0077have hnegative_one_first : ModEq(k,a · f,b · e)
    Exact native replay linehave hnegative_one_first : exists ftcn_left_fssbn_hnegative_one_first ftcn_right_fssbn_hnegative_one_first. (a * f) + (k) * ftcn_left_fssbn_hnegative_one_first = (b * e) + (k) * ftcn_right_fssbn_hnegative_one_first
  78. 0078specialize four_square_signed_cross_negative k
  79. 0079specialize four_square_signed_cross_negative a
  80. 0080specialize four_square_signed_cross_negative b
  81. 0081specialize four_square_signed_cross_negative e
  82. 0082specialize four_square_signed_cross_negative f
  83. 0083apply four_square_signed_cross_negative
  84. 0084exact ha
  85. 0085exact hb
  86. 0086have hnegative_one_second : ModEq(k,c · h,d · g)
    Exact native replay linehave hnegative_one_second : exists ftcn_left_fssbn_hnegative_one_second ftcn_right_fssbn_hnegative_one_second. (c * h) + (k) * ftcn_left_fssbn_hnegative_one_second = (d * g) + (k) * ftcn_right_fssbn_hnegative_one_second
  87. 0087specialize four_square_signed_cross_negative k
  88. 0088specialize four_square_signed_cross_negative c
  89. 0089specialize four_square_signed_cross_negative d
  90. 0090specialize four_square_signed_cross_negative g
  91. 0091specialize four_square_signed_cross_negative h
  92. 0092apply four_square_signed_cross_negative
  93. 0093exact hc
  94. 0094exact hd
  95. 0095specialize mod_eq_add k
  96. 0096specialize mod_eq_add (a * f)
  97. 0097specialize mod_eq_add (b * e)
  98. 0098specialize mod_eq_add (c * h)
  99. 0099specialize mod_eq_add (d * g)
  100. 0100apply mod_eq_add
  101. 0101exact hnegative_one_first
  102. 0102exact hnegative_one_second
  103. 0103split
  104. 0104have hnegative_two_first : ModEq(k,a · g,c · e)
    Exact native replay linehave hnegative_two_first : exists ftcn_left_fssbn_hnegative_two_first ftcn_right_fssbn_hnegative_two_first. (a * g) + (k) * ftcn_left_fssbn_hnegative_two_first = (c * e) + (k) * ftcn_right_fssbn_hnegative_two_first
  105. 0105specialize four_square_signed_cross_negative k
  106. 0106specialize four_square_signed_cross_negative a
  107. 0107specialize four_square_signed_cross_negative c
  108. 0108specialize four_square_signed_cross_negative e
  109. 0109specialize four_square_signed_cross_negative g
  110. 0110apply four_square_signed_cross_negative
  111. 0111exact ha
  112. 0112exact hc
  113. 0113have hnegative_two_second : ModEq(k,d · f,b · h)
    Exact native replay linehave hnegative_two_second : exists ftcn_left_fssbn_hnegative_two_second ftcn_right_fssbn_hnegative_two_second. (d * f) + (k) * ftcn_left_fssbn_hnegative_two_second = (b * h) + (k) * ftcn_right_fssbn_hnegative_two_second
  114. 0114specialize four_square_signed_cross_negative k
  115. 0115specialize four_square_signed_cross_negative d
  116. 0116specialize four_square_signed_cross_negative b
  117. 0117specialize four_square_signed_cross_negative h
  118. 0118specialize four_square_signed_cross_negative f
  119. 0119apply four_square_signed_cross_negative
  120. 0120exact hd
  121. 0121exact hb
  122. 0122specialize mod_eq_add k
  123. 0123specialize mod_eq_add (a * g)
  124. 0124specialize mod_eq_add (c * e)
  125. 0125specialize mod_eq_add (d * f)
  126. 0126specialize mod_eq_add (b * h)
  127. 0127apply mod_eq_add
  128. 0128exact hnegative_two_first
  129. 0129exact hnegative_two_second
  130. 0130have hnegative_three_first : ModEq(k,a · h,d · e)
    Exact native replay linehave hnegative_three_first : exists ftcn_left_fssbn_hnegative_three_first ftcn_right_fssbn_hnegative_three_first. (a * h) + (k) * ftcn_left_fssbn_hnegative_three_first = (d * e) + (k) * ftcn_right_fssbn_hnegative_three_first
  131. 0131specialize four_square_signed_cross_negative k
  132. 0132specialize four_square_signed_cross_negative a
  133. 0133specialize four_square_signed_cross_negative d
  134. 0134specialize four_square_signed_cross_negative e
  135. 0135specialize four_square_signed_cross_negative h
  136. 0136apply four_square_signed_cross_negative
  137. 0137exact ha
  138. 0138exact hd
  139. 0139have hnegative_three_second : ModEq(k,b · g,c · f)
    Exact native replay linehave hnegative_three_second : exists ftcn_left_fssbn_hnegative_three_second ftcn_right_fssbn_hnegative_three_second. (b * g) + (k) * ftcn_left_fssbn_hnegative_three_second = (c * f) + (k) * ftcn_right_fssbn_hnegative_three_second
  140. 0140specialize four_square_signed_cross_negative k
  141. 0141specialize four_square_signed_cross_negative b
  142. 0142specialize four_square_signed_cross_negative c
  143. 0143specialize four_square_signed_cross_negative f
  144. 0144specialize four_square_signed_cross_negative g
  145. 0145apply four_square_signed_cross_negative
  146. 0146exact hb
  147. 0147exact hc
  148. 0148specialize mod_eq_add k
  149. 0149specialize mod_eq_add (a * h)
  150. 0150specialize mod_eq_add (d * e)
  151. 0151specialize mod_eq_add (b * g)
  152. 0152specialize mod_eq_add (c * f)
  153. 0153apply mod_eq_add
  154. 0154exact hnegative_three_first
  155. 0155exact hnegative_three_second