GI0020

gaussian_product_associate_real_positive

Exact real positive component associativity for the actual four-component Gaussian product.

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

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.

The natural-code carrier consists of genuine pairs of the existing signed integers; no new primitive arithmetic is trusted. The theorem constructs quotient, remainder, and actual norm witnesses. Gaussian gcd, unique factorization, and prime classification are separate targets.

Exact theorem in conservative defined notation

∀ a. ∀ b. ∀ c. ∀ d. ∀ e. ∀ f. ∀ g. ∀ h. ∀ i. ∀ j. ∀ k. ∀ l. (a · e + b · f + (c · h + d · g)) · i + (a · f + b · e + (c · g + d · h)) · j + ((a · g + b · h + (c · e + d · f)) · l + (a · h + b · g + (c · f + d · e)) · k) = a · (e · i + f · j + (g · l + h · k)) + b · (e · j + f · i + (g · k + h · l)) + (c · (e · l + f · k + (g · j + h · i)) + d · (e · k + f · l + (g · i + h · j)))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

none

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
Original expanded first-order statement 
forall a b c d e f g h i j k l. ((((((((((((a) * (e))) + (((b) * (f))))) + (((((c) * (h))) + (((d) * (g))))))) * (i))) + (((((((((a) * (f))) + (((b) * (e))))) + (((((c) * (g))) + (((d) * (h))))))) * (j))))) + (((((((((((a) * (g))) + (((b) * (h))))) + (((((c) * (e))) + (((d) * (f))))))) * (l))) + (((((((((a) * (h))) + (((b) * (g))))) + (((((c) * (f))) + (((d) * (e))))))) * (k)))))) = ((((((a) * (((((((e) * (i))) + (((f) * (j))))) + (((((g) * (l))) + (((h) * (k))))))))) + (((b) * (((((((e) * (j))) + (((f) * (i))))) + (((((g) * (k))) + (((h) * (l))))))))))) + (((((c) * (((((((e) * (l))) + (((f) * (k))))) + (((((g) * (j))) + (((h) * (i))))))))) + (((d) * (((((((e) * (k))) + (((f) * (l))))) + (((((g) * (i))) + (((h) * (j))))))))))))

Complete tactic proof in conservative notation

All 216 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

216 script commands · 35 reading checkpoints · 0 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.

01Fix variables and assumptionsL1–10

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

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

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

  1. L11
    intro k
  2. L12
    intro l
03Calculate and transport equalitiesL13–22

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L13
    trans ((((a) * (((e) * (i))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((a) * (((f) * (j))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))))))
  2. L14
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  3. L15
    trans ((((a) * (((e) * (i))))) + ((((a) * (((f) * (j))))) + ((((a) * (((g) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((e) * (j))))) + ((((b) * (((f) * (i))))) + ((((b) * (((g) * (k))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((c) * (((f) * (k))))) + ((((c) * (((g) * (j))))) + ((((c) * (((h) * (i))))) + ((((d) * (((e) * (k))))) + ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + (((d) * (((h) * (j))))))))))))))))))))
  4. L16
    congr
  5. L17
    refl
  6. L18
    trans ((((a) * (((f) * (j))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))))))
  7. L19
    trans ((((b) * (((f) * (i))))) + ((((a) * (((f) * (j))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))))))
  8. L20
    congr
  9. L21
    refl
  10. L22
    trans ((((c) * (((h) * (i))))) + ((((a) * (((f) * (j))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))))
04Calculate and transport equalitiesL23–24

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L23
    congr
  2. L24
    refl
05Use earlier factsL25–27

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

  1. L25
    apply four_square_add_swap_right_tail
  2. L26
    apply four_square_add_swap_right_tail
  3. L27
    apply four_square_add_swap_right_tail
06Calculate and transport equalitiesL28–37

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L28
    congr
  2. L29
    refl
  3. L30
    trans ((((a) * (((g) * (l))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))))
  4. L31
    trans ((((b) * (((f) * (i))))) + ((((a) * (((g) * (l))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))))
  5. L32
    congr
  6. L33
    refl
  7. L34
    trans ((((c) * (((h) * (i))))) + ((((a) * (((g) * (l))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))))
  8. L35
    congr
  9. L36
    refl
  10. L37
    trans ((((d) * (((g) * (i))))) + ((((a) * (((g) * (l))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))
07Calculate and transport equalitiesL38–45

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L38
    congr
  2. L39
    refl
  3. L40
    trans ((((b) * (((e) * (j))))) + ((((a) * (((g) * (l))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))
  4. L41
    congr
  5. L42
    refl
  6. L43
    trans ((((c) * (((g) * (j))))) + ((((a) * (((g) * (l))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))
  7. L44
    congr
  8. L45
    refl
08Use earlier factsL46–51

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

  1. L46
    apply four_square_add_swap_right_tail
  2. L47
    apply four_square_add_swap_right_tail
  3. L48
    apply four_square_add_swap_right_tail
  4. L49
    apply four_square_add_swap_right_tail
  5. L50
    apply four_square_add_swap_right_tail
  6. L51
    apply four_square_add_swap_right_tail
09Calculate and transport equalitiesL52–61

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L52
    congr
  2. L53
    refl
  3. L54
    trans ((((a) * (((h) * (k))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))))
  4. L55
    trans ((((b) * (((f) * (i))))) + ((((a) * (((h) * (k))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))))
  5. L56
    congr
  6. L57
    refl
  7. L58
    trans ((((c) * (((h) * (i))))) + ((((a) * (((h) * (k))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))
  8. L59
    congr
  9. L60
    refl
  10. L61
    trans ((((d) * (((g) * (i))))) + ((((a) * (((h) * (k))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))
10Calculate and transport equalitiesL62–71

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L62
    congr
  2. L63
    refl
  3. L64
    trans ((((b) * (((e) * (j))))) + ((((a) * (((h) * (k))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))
  4. L65
    congr
  5. L66
    refl
  6. L67
    trans ((((c) * (((g) * (j))))) + ((((a) * (((h) * (k))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))
  7. L68
    congr
  8. L69
    refl
  9. L70
    trans ((((d) * (((h) * (j))))) + ((((a) * (((h) * (k))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))
  10. L71
    congr
11Calculate and transport equalitiesL72–78

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L72
    refl
  2. L73
    trans ((((b) * (((h) * (l))))) + ((((a) * (((h) * (k))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))
  3. L74
    congr
  4. L75
    refl
  5. L76
    trans ((((c) * (((e) * (l))))) + ((((a) * (((h) * (k))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))
  6. L77
    congr
  7. L78
    refl
12Use earlier factsL79–87

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

  1. L79
    apply four_square_add_swap_right_tail
  2. L80
    apply four_square_add_swap_right_tail
  3. L81
    apply four_square_add_swap_right_tail
  4. L82
    apply four_square_add_swap_right_tail
  5. L83
    apply four_square_add_swap_right_tail
  6. L84
    apply four_square_add_swap_right_tail
  7. L85
    apply four_square_add_swap_right_tail
  8. L86
    apply four_square_add_swap_right_tail
  9. L87
    apply four_square_add_swap_right_tail
13Calculate and transport equalitiesL88–96

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L88
    congr
  2. L89
    refl
  3. L90
    trans ((((b) * (((e) * (j))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))
  4. L91
    trans ((((b) * (((f) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))
  5. L92
    congr
  6. L93
    refl
  7. L94
    trans ((((c) * (((h) * (i))))) + ((((b) * (((e) * (j))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))
  8. L95
    congr
  9. L96
    refl
14Use earlier factsL97–99

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

  1. L97
    apply four_square_add_swap_right_tail
  2. L98
    apply four_square_add_swap_right_tail
  3. L99
    apply four_square_add_swap_right_tail
15Calculate and transport equalitiesL100–109

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L100
    congr
  2. L101
    refl
  3. L102
    congr
  4. L103
    refl
  5. L104
    trans ((((b) * (((g) * (k))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))
  6. L105
    trans ((((c) * (((h) * (i))))) + ((((b) * (((g) * (k))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))
  7. L106
    congr
  8. L107
    refl
  9. L108
    trans ((((d) * (((g) * (i))))) + ((((b) * (((g) * (k))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))
  10. L109
    congr
16Calculate and transport equalitiesL110–119

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L110
    refl
  2. L111
    trans ((((c) * (((g) * (j))))) + ((((b) * (((g) * (k))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))
  3. L112
    congr
  4. L113
    refl
  5. L114
    trans ((((d) * (((h) * (j))))) + ((((b) * (((g) * (k))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))
  6. L115
    congr
  7. L116
    refl
  8. L117
    trans ((((b) * (((h) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))
  9. L118
    congr
  10. L119
    refl
17Calculate and transport equalitiesL120–122

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L120
    trans ((((c) * (((e) * (l))))) + ((((b) * (((g) * (k))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))
  2. L121
    congr
  3. L122
    refl
18Use earlier factsL123–129

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

  1. L123
    apply four_square_add_swap_right_tail
  2. L124
    apply four_square_add_swap_right_tail
  3. L125
    apply four_square_add_swap_right_tail
  4. L126
    apply four_square_add_swap_right_tail
  5. L127
    apply four_square_add_swap_right_tail
  6. L128
    apply four_square_add_swap_right_tail
  7. L129
    apply four_square_add_swap_right_tail
19Calculate and transport equalitiesL130–139

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L130
    congr
  2. L131
    refl
  3. L132
    trans ((((b) * (((h) * (l))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))
  4. L133
    trans ((((c) * (((h) * (i))))) + ((((b) * (((h) * (l))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))
  5. L134
    congr
  6. L135
    refl
  7. L136
    trans ((((d) * (((g) * (i))))) + ((((b) * (((h) * (l))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))
  8. L137
    congr
  9. L138
    refl
  10. L139
    trans ((((c) * (((g) * (j))))) + ((((b) * (((h) * (l))))) + ((((d) * (((h) * (j))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))
20Calculate and transport equalitiesL140–141

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L140
    congr
  2. L141
    refl
21Use earlier factsL142–145

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

  1. L142
    apply four_square_add_swap_right_tail
  2. L143
    apply four_square_add_swap_right_tail
  3. L144
    apply four_square_add_swap_right_tail
  4. L145
    apply four_square_add_swap_right_tail
22Calculate and transport equalitiesL146–155

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L146
    congr
  2. L147
    refl
  3. L148
    trans ((((c) * (((e) * (l))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))
  4. L149
    trans ((((c) * (((h) * (i))))) + ((((c) * (((e) * (l))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))
  5. L150
    congr
  6. L151
    refl
  7. L152
    trans ((((d) * (((g) * (i))))) + ((((c) * (((e) * (l))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))
  8. L153
    congr
  9. L154
    refl
  10. L155
    trans ((((c) * (((g) * (j))))) + ((((c) * (((e) * (l))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))
23Calculate and transport equalitiesL156–157

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L156
    congr
  2. L157
    refl
24Use earlier factsL158–161

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

  1. L158
    apply four_square_add_swap_right_tail
  2. L159
    apply four_square_add_swap_right_tail
  3. L160
    apply four_square_add_swap_right_tail
  4. L161
    apply four_square_add_swap_right_tail
25Calculate and transport equalitiesL162–171

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L162
    congr
  2. L163
    refl
  3. L164
    trans ((((c) * (((f) * (k))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k)))))))))))
  4. L165
    trans ((((c) * (((h) * (i))))) + ((((c) * (((f) * (k))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k)))))))))))
  5. L166
    congr
  6. L167
    refl
  7. L168
    trans ((((d) * (((g) * (i))))) + ((((c) * (((f) * (k))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k))))))))))
  8. L169
    congr
  9. L170
    refl
  10. L171
    trans ((((c) * (((g) * (j))))) + ((((c) * (((f) * (k))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k)))))))))
26Calculate and transport equalitiesL172–176

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L172
    congr
  2. L173
    refl
  3. L174
    trans ((((d) * (((h) * (j))))) + ((((c) * (((f) * (k))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k))))))))
  4. L175
    congr
  5. L176
    refl
27Use earlier factsL177–181

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

  1. L177
    apply four_square_add_swap_right_tail
  2. L178
    apply four_square_add_swap_right_tail
  3. L179
    apply four_square_add_swap_right_tail
  4. L180
    apply four_square_add_swap_right_tail
  5. L181
    apply four_square_add_swap_right_tail
28Calculate and transport equalitiesL182–187

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L182
    congr
  2. L183
    refl
  3. L184
    trans ((((c) * (((g) * (j))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k))))))))))
  4. L185
    trans ((((c) * (((h) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k))))))))))
  5. L186
    congr
  6. L187
    refl
29Use earlier factsL188–189

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

  1. L188
    apply four_square_add_swap_right_tail
  2. L189
    apply four_square_add_swap_right_tail
30Calculate and transport equalitiesL190–199

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L190
    congr
  2. L191
    refl
  3. L192
    congr
  4. L193
    refl
  5. L194
    trans ((((d) * (((e) * (k))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + (((d) * (((f) * (l))))))))
  6. L195
    trans ((((d) * (((g) * (i))))) + ((((d) * (((e) * (k))))) + ((((d) * (((h) * (j))))) + (((d) * (((f) * (l))))))))
  7. L196
    congr
  8. L197
    refl
  9. L198
    trans ((((d) * (((h) * (j))))) + ((((d) * (((e) * (k))))) + (((d) * (((f) * (l)))))))
  10. L199
    congr
31Calculate and transport equalitiesL200–200

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L200
    refl
32Use earlier factsL201–203

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

  1. L201
    apply add_comm
  2. L202
    apply four_square_add_swap_right_tail
  3. L203
    apply four_square_add_swap_right_tail
33Calculate and transport equalitiesL204–209

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L204
    congr
  2. L205
    refl
  3. L206
    trans ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + (((d) * (((h) * (j)))))))
  4. L207
    trans ((((d) * (((g) * (i))))) + ((((d) * (((f) * (l))))) + (((d) * (((h) * (j)))))))
  5. L208
    congr
  6. L209
    refl
34Use earlier factsL210–211

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

  1. L210
    apply add_comm
  2. L211
    apply four_square_add_swap_right_tail
35Calculate and transport equalitiesL212–216

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L212
    congr
  2. L213
    refl
  3. L214
    refl
  4. L215
    symm
  5. L216
    simp [add_mul, mul_add, mul_assoc, add_assoc]

Library-wide reading audit

Original defined command ledger · 216 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro f
  7. 0007intro g
  8. 0008intro h
  9. 0009intro i
  10. 0010intro j
  11. 0011intro k
  12. 0012intro l
  13. 0013trans ((((a) * (((e) * (i))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((a) * (((f) * (j))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))))))
  14. 0014simp [add_mul, mul_add, mul_assoc, add_assoc]
  15. 0015trans ((((a) * (((e) * (i))))) + ((((a) * (((f) * (j))))) + ((((a) * (((g) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((e) * (j))))) + ((((b) * (((f) * (i))))) + ((((b) * (((g) * (k))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((c) * (((f) * (k))))) + ((((c) * (((g) * (j))))) + ((((c) * (((h) * (i))))) + ((((d) * (((e) * (k))))) + ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + (((d) * (((h) * (j))))))))))))))))))))
  16. 0016congr
  17. 0017refl
  18. 0018trans ((((a) * (((f) * (j))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))))))
  19. 0019trans ((((b) * (((f) * (i))))) + ((((a) * (((f) * (j))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))))))
  20. 0020congr
  21. 0021refl
  22. 0022trans ((((c) * (((h) * (i))))) + ((((a) * (((f) * (j))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((a) * (((g) * (l))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))))
  23. 0023congr
  24. 0024refl
  25. 0025apply four_square_add_swap_right_tail
  26. 0026apply four_square_add_swap_right_tail
  27. 0027apply four_square_add_swap_right_tail
  28. 0028congr
  29. 0029refl
  30. 0030trans ((((a) * (((g) * (l))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))))
  31. 0031trans ((((b) * (((f) * (i))))) + ((((a) * (((g) * (l))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))))
  32. 0032congr
  33. 0033refl
  34. 0034trans ((((c) * (((h) * (i))))) + ((((a) * (((g) * (l))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))))
  35. 0035congr
  36. 0036refl
  37. 0037trans ((((d) * (((g) * (i))))) + ((((a) * (((g) * (l))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))
  38. 0038congr
  39. 0039refl
  40. 0040trans ((((b) * (((e) * (j))))) + ((((a) * (((g) * (l))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))
  41. 0041congr
  42. 0042refl
  43. 0043trans ((((c) * (((g) * (j))))) + ((((a) * (((g) * (l))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((a) * (((h) * (k))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))
  44. 0044congr
  45. 0045refl
  46. 0046apply four_square_add_swap_right_tail
  47. 0047apply four_square_add_swap_right_tail
  48. 0048apply four_square_add_swap_right_tail
  49. 0049apply four_square_add_swap_right_tail
  50. 0050apply four_square_add_swap_right_tail
  51. 0051apply four_square_add_swap_right_tail
  52. 0052congr
  53. 0053refl
  54. 0054trans ((((a) * (((h) * (k))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))))
  55. 0055trans ((((b) * (((f) * (i))))) + ((((a) * (((h) * (k))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))))
  56. 0056congr
  57. 0057refl
  58. 0058trans ((((c) * (((h) * (i))))) + ((((a) * (((h) * (k))))) + ((((d) * (((g) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))
  59. 0059congr
  60. 0060refl
  61. 0061trans ((((d) * (((g) * (i))))) + ((((a) * (((h) * (k))))) + ((((b) * (((e) * (j))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))
  62. 0062congr
  63. 0063refl
  64. 0064trans ((((b) * (((e) * (j))))) + ((((a) * (((h) * (k))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))
  65. 0065congr
  66. 0066refl
  67. 0067trans ((((c) * (((g) * (j))))) + ((((a) * (((h) * (k))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))
  68. 0068congr
  69. 0069refl
  70. 0070trans ((((d) * (((h) * (j))))) + ((((a) * (((h) * (k))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))
  71. 0071congr
  72. 0072refl
  73. 0073trans ((((b) * (((h) * (l))))) + ((((a) * (((h) * (k))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))
  74. 0074congr
  75. 0075refl
  76. 0076trans ((((c) * (((e) * (l))))) + ((((a) * (((h) * (k))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))
  77. 0077congr
  78. 0078refl
  79. 0079apply four_square_add_swap_right_tail
  80. 0080apply four_square_add_swap_right_tail
  81. 0081apply four_square_add_swap_right_tail
  82. 0082apply four_square_add_swap_right_tail
  83. 0083apply four_square_add_swap_right_tail
  84. 0084apply four_square_add_swap_right_tail
  85. 0085apply four_square_add_swap_right_tail
  86. 0086apply four_square_add_swap_right_tail
  87. 0087apply four_square_add_swap_right_tail
  88. 0088congr
  89. 0089refl
  90. 0090trans ((((b) * (((e) * (j))))) + ((((b) * (((f) * (i))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))
  91. 0091trans ((((b) * (((f) * (i))))) + ((((b) * (((e) * (j))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))))
  92. 0092congr
  93. 0093refl
  94. 0094trans ((((c) * (((h) * (i))))) + ((((b) * (((e) * (j))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))))
  95. 0095congr
  96. 0096refl
  97. 0097apply four_square_add_swap_right_tail
  98. 0098apply four_square_add_swap_right_tail
  99. 0099apply four_square_add_swap_right_tail
  100. 0100congr
  101. 0101refl
  102. 0102congr
  103. 0103refl
  104. 0104trans ((((b) * (((g) * (k))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))
  105. 0105trans ((((c) * (((h) * (i))))) + ((((b) * (((g) * (k))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))))
  106. 0106congr
  107. 0107refl
  108. 0108trans ((((d) * (((g) * (i))))) + ((((b) * (((g) * (k))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))
  109. 0109congr
  110. 0110refl
  111. 0111trans ((((c) * (((g) * (j))))) + ((((b) * (((g) * (k))))) + ((((d) * (((h) * (j))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))
  112. 0112congr
  113. 0113refl
  114. 0114trans ((((d) * (((h) * (j))))) + ((((b) * (((g) * (k))))) + ((((b) * (((h) * (l))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))
  115. 0115congr
  116. 0116refl
  117. 0117trans ((((b) * (((h) * (l))))) + ((((b) * (((g) * (k))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))
  118. 0118congr
  119. 0119refl
  120. 0120trans ((((c) * (((e) * (l))))) + ((((b) * (((g) * (k))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))
  121. 0121congr
  122. 0122refl
  123. 0123apply four_square_add_swap_right_tail
  124. 0124apply four_square_add_swap_right_tail
  125. 0125apply four_square_add_swap_right_tail
  126. 0126apply four_square_add_swap_right_tail
  127. 0127apply four_square_add_swap_right_tail
  128. 0128apply four_square_add_swap_right_tail
  129. 0129apply four_square_add_swap_right_tail
  130. 0130congr
  131. 0131refl
  132. 0132trans ((((b) * (((h) * (l))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))
  133. 0133trans ((((c) * (((h) * (i))))) + ((((b) * (((h) * (l))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))))
  134. 0134congr
  135. 0135refl
  136. 0136trans ((((d) * (((g) * (i))))) + ((((b) * (((h) * (l))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))
  137. 0137congr
  138. 0138refl
  139. 0139trans ((((c) * (((g) * (j))))) + ((((b) * (((h) * (l))))) + ((((d) * (((h) * (j))))) + ((((c) * (((e) * (l))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))
  140. 0140congr
  141. 0141refl
  142. 0142apply four_square_add_swap_right_tail
  143. 0143apply four_square_add_swap_right_tail
  144. 0144apply four_square_add_swap_right_tail
  145. 0145apply four_square_add_swap_right_tail
  146. 0146congr
  147. 0147refl
  148. 0148trans ((((c) * (((e) * (l))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))
  149. 0149trans ((((c) * (((h) * (i))))) + ((((c) * (((e) * (l))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))))
  150. 0150congr
  151. 0151refl
  152. 0152trans ((((d) * (((g) * (i))))) + ((((c) * (((e) * (l))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k)))))))))))
  153. 0153congr
  154. 0154refl
  155. 0155trans ((((c) * (((g) * (j))))) + ((((c) * (((e) * (l))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + ((((c) * (((f) * (k))))) + (((d) * (((e) * (k))))))))))
  156. 0156congr
  157. 0157refl
  158. 0158apply four_square_add_swap_right_tail
  159. 0159apply four_square_add_swap_right_tail
  160. 0160apply four_square_add_swap_right_tail
  161. 0161apply four_square_add_swap_right_tail
  162. 0162congr
  163. 0163refl
  164. 0164trans ((((c) * (((f) * (k))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k)))))))))))
  165. 0165trans ((((c) * (((h) * (i))))) + ((((c) * (((f) * (k))))) + ((((d) * (((g) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k)))))))))))
  166. 0166congr
  167. 0167refl
  168. 0168trans ((((d) * (((g) * (i))))) + ((((c) * (((f) * (k))))) + ((((c) * (((g) * (j))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k))))))))))
  169. 0169congr
  170. 0170refl
  171. 0171trans ((((c) * (((g) * (j))))) + ((((c) * (((f) * (k))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k)))))))))
  172. 0172congr
  173. 0173refl
  174. 0174trans ((((d) * (((h) * (j))))) + ((((c) * (((f) * (k))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k))))))))
  175. 0175congr
  176. 0176refl
  177. 0177apply four_square_add_swap_right_tail
  178. 0178apply four_square_add_swap_right_tail
  179. 0179apply four_square_add_swap_right_tail
  180. 0180apply four_square_add_swap_right_tail
  181. 0181apply four_square_add_swap_right_tail
  182. 0182congr
  183. 0183refl
  184. 0184trans ((((c) * (((g) * (j))))) + ((((c) * (((h) * (i))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k))))))))))
  185. 0185trans ((((c) * (((h) * (i))))) + ((((c) * (((g) * (j))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + ((((d) * (((f) * (l))))) + (((d) * (((e) * (k))))))))))
  186. 0186congr
  187. 0187refl
  188. 0188apply four_square_add_swap_right_tail
  189. 0189apply four_square_add_swap_right_tail
  190. 0190congr
  191. 0191refl
  192. 0192congr
  193. 0193refl
  194. 0194trans ((((d) * (((e) * (k))))) + ((((d) * (((g) * (i))))) + ((((d) * (((h) * (j))))) + (((d) * (((f) * (l))))))))
  195. 0195trans ((((d) * (((g) * (i))))) + ((((d) * (((e) * (k))))) + ((((d) * (((h) * (j))))) + (((d) * (((f) * (l))))))))
  196. 0196congr
  197. 0197refl
  198. 0198trans ((((d) * (((h) * (j))))) + ((((d) * (((e) * (k))))) + (((d) * (((f) * (l)))))))
  199. 0199congr
  200. 0200refl
  201. 0201apply add_comm
  202. 0202apply four_square_add_swap_right_tail
  203. 0203apply four_square_add_swap_right_tail
  204. 0204congr
  205. 0205refl
  206. 0206trans ((((d) * (((f) * (l))))) + ((((d) * (((g) * (i))))) + (((d) * (((h) * (j)))))))
  207. 0207trans ((((d) * (((g) * (i))))) + ((((d) * (((f) * (l))))) + (((d) * (((h) * (j)))))))
  208. 0208congr
  209. 0209refl
  210. 0210apply add_comm
  211. 0211apply four_square_add_swap_right_tail
  212. 0212congr
  213. 0213refl
  214. 0214refl
  215. 0215symm
  216. 0216simp [add_mul, mul_add, mul_assoc, add_assoc]