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.
A floor quotient in the fundamental parallelogram already gives the required strict norm decrease; global nearest-point optimality is not asserted. The shared carrier is identical to the Gaussian carrier, but the multiplication law and norm are different. Eisenstein gcd, factorization, and prime classification remain separate targets.
Exact theorem in conservative defined notation
∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. EisensteinCoordinateProduct(d,c,a + d,b + c,e,f,g,h,a · h + b · g + (c · f + d · e) + (c · g + d · h),a · g + b · h + (c · e + d · f) + (c · h + d · g),a · e + b · f + (c · h + d · g) + (a · h + b · g + (c · f + d · e) + (c · g + d · h)),a · f + b · e + (c · g + d · h) + (a · g + b · h + (c · e + d · f) + (c · h + d · g)))Every linked abbreviation expands hygienically to the identical original native formula.
Definition DAG
Actual proof prerequisites
add_mul · checked external prerequisitemul_add · checked external prerequisitemul_assoc · checked external prerequisiteadd_assoc · checked external prerequisiteadd_comm · checked external prerequisitefour_square_add_swap_right_tail · checked external prerequisite
Complete tactic proof in conservative notation
All 329 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.
Read the argument
Proof checkpoints
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.
01Fix variables and assumptionsL1–8
02Separate the logical casesL9–9
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L9
split
03Calculate and transport equalitiesL10–19
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L10
trans ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))) - L11
simp [add_mul, mul_add, mul_assoc, add_assoc] - L12
trans ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))) - L13
congr - L14
refl - L15
congr - L16
refl - L17
congr - L18
refl - L19
congr
04Calculate and transport equalitiesL20–29
05Calculate and transport equalitiesL30–39
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L30
refl - L31
congr - L32
refl - L33
congr - L34
refl - L35
refl - L36
trans ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((d) * (f))) + ((((c) * (e))) + ((((a) * (g))) + ((((d) * (g))) + ((((b) * (h))) + (((c) * (h)))))))))))))) - L37
trans ((((a) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))) - L38
trans ((((d) * (e))) + ((((a) * (h))) + ((((c) * (f))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))) - L39
congr
06Calculate and transport equalitiesL40–40
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L40
refl
07Use earlier factsL41–42
08Calculate and transport equalitiesL43–51
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L43
congr - L44
refl - L45
trans ((((b) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))) - L46
trans ((((d) * (e))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))) - L47
congr - L48
refl - L49
trans ((((c) * (f))) + ((((b) * (g))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))) - L50
congr - L51
refl
09Use earlier factsL52–54
10Calculate and transport equalitiesL55–57
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
11Use earlier factsL58–58
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L58
apply four_square_add_swap_right_tail
12Calculate and transport equalitiesL59–63
13Use earlier factsL64–64
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L64
apply four_square_add_swap_right_tail
14Calculate and transport equalitiesL65–74
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L65
congr - L66
refl - L67
congr - L68
refl - L69
trans ((((d) * (f))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g)))))))) - L70
trans ((((a) * (g))) + ((((d) * (f))) + ((((b) * (h))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g)))))))) - L71
congr - L72
refl - L73
trans ((((b) * (h))) + ((((d) * (f))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g))))))) - L74
congr
15Calculate and transport equalitiesL75–75
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L75
refl
16Use earlier factsL76–78
17Calculate and transport equalitiesL79–84
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
18Use earlier factsL85–86
19Calculate and transport equalitiesL87–94
20Use earlier factsL95–96
21Calculate and transport equalitiesL97–106
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
22Calculate and transport equalitiesL107–116
23Calculate and transport equalitiesL117–126
24Calculate and transport equalitiesL127–136
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L127
trans ((((d) * (g))) + ((((c) * (h))) + ((((a) * (e))) + ((((d) * (e))) + ((((b) * (f))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))))) - L128
simp [add_mul, mul_add, mul_assoc, add_assoc] - L129
trans ((((d) * (g))) + ((((c) * (h))) + ((((a) * (e))) + ((((d) * (e))) + ((((b) * (f))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))))) - L130
congr - L131
refl - L132
congr - L133
refl - L134
congr - L135
refl - L136
congr
25Calculate and transport equalitiesL137–146
26Calculate and transport equalitiesL147–156
27Calculate and transport equalitiesL157–166
28Calculate and transport equalitiesL167–173
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L167
refl - L168
refl - L169
trans ((((a) * (e))) + ((((b) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((d) * (f))) + ((((b) * (e))) + ((((c) * (e))) + ((((a) * (g))) + ((((d) * (g))) + ((((b) * (h))) + (((c) * (h)))))))))))))))))))))) - L170
trans ((((a) * (e))) + ((((d) * (g))) + ((((c) * (h))) + ((((d) * (e))) + ((((b) * (f))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))))) - L171
trans ((((d) * (g))) + ((((a) * (e))) + ((((c) * (h))) + ((((d) * (e))) + ((((b) * (f))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))))) - L172
congr - L173
refl
29Use earlier factsL174–175
30Calculate and transport equalitiesL176–184
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L176
congr - L177
refl - L178
trans ((((b) * (f))) + ((((d) * (g))) + ((((c) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))))))))))) - L179
trans ((((d) * (g))) + ((((b) * (f))) + ((((c) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))))))))))) - L180
congr - L181
refl - L182
trans ((((c) * (h))) + ((((b) * (f))) + ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))) - L183
congr - L184
refl
31Use earlier factsL185–187
32Calculate and transport equalitiesL188–190
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L188
congr - L189
refl - L190
trans ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))))))))))
33Use earlier factsL191–191
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L191
apply four_square_add_swap_right_tail
34Calculate and transport equalitiesL192–199
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L192
congr - L193
refl - L194
congr - L195
refl - L196
trans ((((a) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))) - L197
trans ((((d) * (e))) + ((((a) * (h))) + ((((c) * (f))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))) - L198
congr - L199
refl
35Use earlier factsL200–201
36Calculate and transport equalitiesL202–210
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L202
congr - L203
refl - L204
trans ((((b) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))))))) - L205
trans ((((d) * (e))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))))))) - L206
congr - L207
refl - L208
trans ((((c) * (f))) + ((((b) * (g))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))) - L209
congr - L210
refl
37Use earlier factsL211–213
38Calculate and transport equalitiesL214–216
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
39Use earlier factsL217–217
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L217
apply four_square_add_swap_right_tail
40Calculate and transport equalitiesL218–222
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
41Use earlier factsL223–223
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L223
apply four_square_add_swap_right_tail
42Calculate and transport equalitiesL224–233
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L224
congr - L225
refl - L226
congr - L227
refl - L228
trans ((((d) * (h))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))) - L229
trans ((((a) * (f))) + ((((d) * (h))) + ((((b) * (e))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))) - L230
congr - L231
refl - L232
trans ((((b) * (e))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))) - L233
congr
43Calculate and transport equalitiesL234–234
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L234
refl
44Use earlier factsL235–237
45Calculate and transport equalitiesL238–243
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L238
congr - L239
refl - L240
trans ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))) - L241
trans ((((a) * (f))) + ((((c) * (g))) + ((((b) * (e))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))) - L242
congr - L243
refl
46Use earlier factsL244–245
47Calculate and transport equalitiesL246–255
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L246
congr - L247
refl - L248
congr - L249
refl - L250
trans ((((d) * (f))) + ((((b) * (e))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g))))))))) - L251
trans ((((b) * (e))) + ((((d) * (f))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g))))))))) - L252
congr - L253
refl - L254
trans ((((a) * (g))) + ((((d) * (f))) + ((((b) * (h))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g)))))))) - L255
congr
48Calculate and transport equalitiesL256–259
49Use earlier factsL260–263
50Calculate and transport equalitiesL264–271
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
51Use earlier factsL272–273
52Calculate and transport equalitiesL274–281
53Use earlier factsL282–283
54Calculate and transport equalitiesL284–293
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L284
congr - L285
refl - L286
refl - L287
trans ((((a) * (e))) + ((((b) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((d) * (f))) + ((((b) * (e))) + ((((c) * (e))) + ((((a) * (g))) + ((((d) * (g))) + ((((b) * (h))) + (((c) * (h)))))))))))))))))))))) - L288
symm - L289
congr - L290
refl - L291
congr - L292
refl - L293
congr
55Calculate and transport equalitiesL294–303
56Calculate and transport equalitiesL304–313
57Calculate and transport equalitiesL314–323
Original defined command ledger · 329 lines
- 0001
intro a - 0002
intro b - 0003
intro c - 0004
intro d - 0005
intro e - 0006
intro f - 0007
intro g - 0008
intro h - 0009
split - 0010
trans ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))) - 0011
simp [add_mul, mul_add, mul_assoc, add_assoc] - 0012
trans ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))) - 0013
congr - 0014
refl - 0015
congr - 0016
refl - 0017
congr - 0018
refl - 0019
congr - 0020
refl - 0021
congr - 0022
refl - 0023
congr - 0024
refl - 0025
congr - 0026
refl - 0027
congr - 0028
refl - 0029
congr - 0030
refl - 0031
congr - 0032
refl - 0033
congr - 0034
refl - 0035
refl - 0036
trans ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((d) * (f))) + ((((c) * (e))) + ((((a) * (g))) + ((((d) * (g))) + ((((b) * (h))) + (((c) * (h)))))))))))))) - 0037
trans ((((a) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))) - 0038
trans ((((d) * (e))) + ((((a) * (h))) + ((((c) * (f))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))) - 0039
congr - 0040
refl - 0041
apply four_square_add_swap_right_tail - 0042
apply four_square_add_swap_right_tail - 0043
congr - 0044
refl - 0045
trans ((((b) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))) - 0046
trans ((((d) * (e))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))) - 0047
congr - 0048
refl - 0049
trans ((((c) * (f))) + ((((b) * (g))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))) - 0050
congr - 0051
refl - 0052
apply four_square_add_swap_right_tail - 0053
apply four_square_add_swap_right_tail - 0054
apply four_square_add_swap_right_tail - 0055
congr - 0056
refl - 0057
trans ((((c) * (f))) + ((((d) * (e))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))) - 0058
apply four_square_add_swap_right_tail - 0059
congr - 0060
refl - 0061
congr - 0062
refl - 0063
trans ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))) - 0064
apply four_square_add_swap_right_tail - 0065
congr - 0066
refl - 0067
congr - 0068
refl - 0069
trans ((((d) * (f))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g)))))))) - 0070
trans ((((a) * (g))) + ((((d) * (f))) + ((((b) * (h))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g)))))))) - 0071
congr - 0072
refl - 0073
trans ((((b) * (h))) + ((((d) * (f))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g))))))) - 0074
congr - 0075
refl - 0076
apply four_square_add_swap_right_tail - 0077
apply four_square_add_swap_right_tail - 0078
apply four_square_add_swap_right_tail - 0079
congr - 0080
refl - 0081
trans ((((c) * (e))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (h))) + (((d) * (g))))))) - 0082
trans ((((a) * (g))) + ((((c) * (e))) + ((((b) * (h))) + ((((c) * (h))) + (((d) * (g))))))) - 0083
congr - 0084
refl - 0085
apply four_square_add_swap_right_tail - 0086
apply four_square_add_swap_right_tail - 0087
congr - 0088
refl - 0089
congr - 0090
refl - 0091
trans ((((d) * (g))) + ((((b) * (h))) + (((c) * (h))))) - 0092
trans ((((b) * (h))) + ((((d) * (g))) + (((c) * (h))))) - 0093
congr - 0094
refl - 0095
apply add_comm - 0096
apply four_square_add_swap_right_tail - 0097
congr - 0098
refl - 0099
refl - 0100
trans ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((d) * (f))) + ((((c) * (e))) + ((((a) * (g))) + ((((d) * (g))) + ((((b) * (h))) + (((c) * (h)))))))))))))) - 0101
symm - 0102
congr - 0103
refl - 0104
congr - 0105
refl - 0106
congr - 0107
refl - 0108
congr - 0109
refl - 0110
congr - 0111
refl - 0112
congr - 0113
refl - 0114
congr - 0115
refl - 0116
congr - 0117
refl - 0118
congr - 0119
refl - 0120
congr - 0121
refl - 0122
congr - 0123
refl - 0124
refl - 0125
symm - 0126
simp [add_mul, mul_add, mul_assoc, add_assoc] - 0127
trans ((((d) * (g))) + ((((c) * (h))) + ((((a) * (e))) + ((((d) * (e))) + ((((b) * (f))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))))) - 0128
simp [add_mul, mul_add, mul_assoc, add_assoc] - 0129
trans ((((d) * (g))) + ((((c) * (h))) + ((((a) * (e))) + ((((d) * (e))) + ((((b) * (f))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))))) - 0130
congr - 0131
refl - 0132
congr - 0133
refl - 0134
congr - 0135
refl - 0136
congr - 0137
refl - 0138
congr - 0139
refl - 0140
congr - 0141
refl - 0142
congr - 0143
refl - 0144
congr - 0145
refl - 0146
congr - 0147
refl - 0148
congr - 0149
refl - 0150
congr - 0151
refl - 0152
congr - 0153
refl - 0154
congr - 0155
refl - 0156
congr - 0157
refl - 0158
congr - 0159
refl - 0160
congr - 0161
refl - 0162
congr - 0163
refl - 0164
congr - 0165
refl - 0166
congr - 0167
refl - 0168
refl - 0169
trans ((((a) * (e))) + ((((b) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((d) * (f))) + ((((b) * (e))) + ((((c) * (e))) + ((((a) * (g))) + ((((d) * (g))) + ((((b) * (h))) + (((c) * (h)))))))))))))))))))))) - 0170
trans ((((a) * (e))) + ((((d) * (g))) + ((((c) * (h))) + ((((d) * (e))) + ((((b) * (f))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))))) - 0171
trans ((((d) * (g))) + ((((a) * (e))) + ((((c) * (h))) + ((((d) * (e))) + ((((b) * (f))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))))) - 0172
congr - 0173
refl - 0174
apply four_square_add_swap_right_tail - 0175
apply four_square_add_swap_right_tail - 0176
congr - 0177
refl - 0178
trans ((((b) * (f))) + ((((d) * (g))) + ((((c) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))))))))))) - 0179
trans ((((d) * (g))) + ((((b) * (f))) + ((((c) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))))))))))) - 0180
congr - 0181
refl - 0182
trans ((((c) * (h))) + ((((b) * (f))) + ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))) - 0183
congr - 0184
refl - 0185
apply four_square_add_swap_right_tail - 0186
apply four_square_add_swap_right_tail - 0187
apply four_square_add_swap_right_tail - 0188
congr - 0189
refl - 0190
trans ((((c) * (h))) + ((((d) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((a) * (h))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))))) - 0191
apply four_square_add_swap_right_tail - 0192
congr - 0193
refl - 0194
congr - 0195
refl - 0196
trans ((((a) * (h))) + ((((d) * (e))) + ((((c) * (f))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))) - 0197
trans ((((d) * (e))) + ((((a) * (h))) + ((((c) * (f))) + ((((d) * (h))) + ((((b) * (g))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))))) - 0198
congr - 0199
refl - 0200
apply four_square_add_swap_right_tail - 0201
apply four_square_add_swap_right_tail - 0202
congr - 0203
refl - 0204
trans ((((b) * (g))) + ((((d) * (e))) + ((((c) * (f))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))))))) - 0205
trans ((((d) * (e))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))))))))) - 0206
congr - 0207
refl - 0208
trans ((((c) * (f))) + ((((b) * (g))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))) - 0209
congr - 0210
refl - 0211
apply four_square_add_swap_right_tail - 0212
apply four_square_add_swap_right_tail - 0213
apply four_square_add_swap_right_tail - 0214
congr - 0215
refl - 0216
trans ((((c) * (f))) + ((((d) * (e))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))))) - 0217
apply four_square_add_swap_right_tail - 0218
congr - 0219
refl - 0220
congr - 0221
refl - 0222
trans ((((c) * (g))) + ((((d) * (h))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))))) - 0223
apply four_square_add_swap_right_tail - 0224
congr - 0225
refl - 0226
congr - 0227
refl - 0228
trans ((((d) * (h))) + ((((a) * (f))) + ((((b) * (e))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))) - 0229
trans ((((a) * (f))) + ((((d) * (h))) + ((((b) * (e))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g)))))))))))) - 0230
congr - 0231
refl - 0232
trans ((((b) * (e))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))) - 0233
congr - 0234
refl - 0235
apply four_square_add_swap_right_tail - 0236
apply four_square_add_swap_right_tail - 0237
apply four_square_add_swap_right_tail - 0238
congr - 0239
refl - 0240
trans ((((c) * (g))) + ((((a) * (f))) + ((((b) * (e))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))) - 0241
trans ((((a) * (f))) + ((((c) * (g))) + ((((b) * (e))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((d) * (f))) + ((((c) * (h))) + (((d) * (g))))))))))) - 0242
congr - 0243
refl - 0244
apply four_square_add_swap_right_tail - 0245
apply four_square_add_swap_right_tail - 0246
congr - 0247
refl - 0248
congr - 0249
refl - 0250
trans ((((d) * (f))) + ((((b) * (e))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g))))))))) - 0251
trans ((((b) * (e))) + ((((d) * (f))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g))))))))) - 0252
congr - 0253
refl - 0254
trans ((((a) * (g))) + ((((d) * (f))) + ((((b) * (h))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g)))))))) - 0255
congr - 0256
refl - 0257
trans ((((b) * (h))) + ((((d) * (f))) + ((((c) * (e))) + ((((c) * (h))) + (((d) * (g))))))) - 0258
congr - 0259
refl - 0260
apply four_square_add_swap_right_tail - 0261
apply four_square_add_swap_right_tail - 0262
apply four_square_add_swap_right_tail - 0263
apply four_square_add_swap_right_tail - 0264
congr - 0265
refl - 0266
congr - 0267
refl - 0268
trans ((((c) * (e))) + ((((a) * (g))) + ((((b) * (h))) + ((((c) * (h))) + (((d) * (g))))))) - 0269
trans ((((a) * (g))) + ((((c) * (e))) + ((((b) * (h))) + ((((c) * (h))) + (((d) * (g))))))) - 0270
congr - 0271
refl - 0272
apply four_square_add_swap_right_tail - 0273
apply four_square_add_swap_right_tail - 0274
congr - 0275
refl - 0276
congr - 0277
refl - 0278
trans ((((d) * (g))) + ((((b) * (h))) + (((c) * (h))))) - 0279
trans ((((b) * (h))) + ((((d) * (g))) + (((c) * (h))))) - 0280
congr - 0281
refl - 0282
apply add_comm - 0283
apply four_square_add_swap_right_tail - 0284
congr - 0285
refl - 0286
refl - 0287
trans ((((a) * (e))) + ((((b) * (f))) + ((((c) * (h))) + ((((d) * (g))) + ((((a) * (h))) + ((((b) * (g))) + ((((c) * (f))) + ((((d) * (e))) + ((((c) * (g))) + ((((d) * (h))) + ((((d) * (h))) + ((((c) * (g))) + ((((a) * (f))) + ((((d) * (f))) + ((((b) * (e))) + ((((c) * (e))) + ((((a) * (g))) + ((((d) * (g))) + ((((b) * (h))) + (((c) * (h)))))))))))))))))))))) - 0288
symm - 0289
congr - 0290
refl - 0291
congr - 0292
refl - 0293
congr - 0294
refl - 0295
congr - 0296
refl - 0297
congr - 0298
refl - 0299
congr - 0300
refl - 0301
congr - 0302
refl - 0303
congr - 0304
refl - 0305
congr - 0306
refl - 0307
congr - 0308
refl - 0309
congr - 0310
refl - 0311
congr - 0312
refl - 0313
congr - 0314
refl - 0315
congr - 0316
refl - 0317
congr - 0318
refl - 0319
congr - 0320
refl - 0321
congr - 0322
refl - 0323
congr - 0324
refl - 0325
congr - 0326
refl - 0327
refl - 0328
symm - 0329
simp [add_mul, mul_add, mul_assoc, add_assoc]