FS000V

four_square_conjugate_diagonal_regroup

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

The conjugate quaternion's sixteen diagonal squares regroup into the exact row-major norm-product diagonal.

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.

Exact expanded first-order arithmetic statement

forall a b c d e f g h. (((((((((a * e) * (a * e)) + ((b * f) * (b * f))) + ((c * g) * (c * g))) + ((d * h) * (d * h)))) + ((((((a * f) * (a * f)) + ((c * h) * (c * h)))) + ((((b * e) * (b * e)) + ((d * g) * (d * g))))))) + (((((((a * g) * (a * g)) + ((d * f) * (d * f)))) + ((((c * e) * (c * e)) + ((b * h) * (b * h)))))) + ((((((a * h) * (a * h)) + ((b * g) * (b * g)))) + ((((d * e) * (d * e)) + ((c * f) * (c * f))))))))) = ((((((((((a * e) * (a * e)) + ((a * f) * (a * f))) + ((a * g) * (a * g))) + ((a * h) * (a * h)))) + ((((((b * e) * (b * e)) + ((b * f) * (b * f))) + ((b * g) * (b * g))) + ((b * h) * (b * h))))) + ((((((c * e) * (c * e)) + ((c * f) * (c * f))) + ((c * g) * (c * g))) + ((c * h) * (c * h))))) + ((((((d * e) * (d * e)) + ((d * f) * (d * f))) + ((d * g) * (d * g))) + ((d * h) * (d * h))))))

Constructive proof overview

Generated structural guide

The conjugate quaternion's sixteen diagonal squares regroup into the exact row-major norm-product diagonal.

The unchanged tactic script uses 3 declared prerequisites and contains 232 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Historical empty-context replay experiment only; that experiment persisted no certificate and granted no release authority. Current checked use follows separately sealed, independently verified proof bundles; there is no Stable promotion.

Proof neighborhood

Direct dependencies

add_assoc Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized FS0006 four_square_add_swap_right_tail

Direct dependents

FS0010 four_square_conjugate_global_compensation

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

232 script commands · 36 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.

Named ingredients (1)
four square add swap right tail
01Fix variables and assumptionsL1–8

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
02Calculate and transport equalitiesL9–18

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

  1. L9
    trans (((a * e) * (a * e)) + (((b * f) * (b * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((a * f) * (a * f)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((a * g) * (a * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))))))
  2. L10
    simp [add_assoc]
  3. L11
    trans (((a * e) * (a * e)) + (((a * f) * (a * f)) + (((a * g) * (a * g)) + (((a * h) * (a * h)) + (((b * e) * (b * e)) + (((b * f) * (b * f)) + (((b * g) * (b * g)) + (((b * h) * (b * h)) + (((c * e) * (c * e)) + (((c * f) * (c * f)) + (((c * g) * (c * g)) + (((c * h) * (c * h)) + (((d * e) * (d * e)) + (((d * f) * (d * f)) + (((d * g) * (d * g)) + ((d * h) * (d * h)))))))))))))))))
  4. L12
    congr
  5. L13
    refl
  6. L14
    trans (((a * f) * (a * f)) + (((b * f) * (b * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((a * g) * (a * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))))))
  7. L15
    trans (((b * f) * (b * f)) + (((a * f) * (a * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((a * g) * (a * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))))))
  8. L16
    congr
  9. L17
    refl
  10. L18
    trans (((c * g) * (c * g)) + (((a * f) * (a * f)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((a * g) * (a * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))))
03Calculate and transport equalitiesL19–20

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

  1. L19
    congr
  2. L20
    refl
04Use earlier factsL21–23

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

  1. L21
    apply four_square_add_swap_right_tail
  2. L22
    apply four_square_add_swap_right_tail
  3. L23
    apply four_square_add_swap_right_tail
05Calculate and transport equalitiesL24–33

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

  1. L24
    congr
  2. L25
    refl
  3. L26
    trans (((a * g) * (a * g)) + (((b * f) * (b * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))))
  4. L27
    trans (((b * f) * (b * f)) + (((a * g) * (a * g)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))))
  5. L28
    congr
  6. L29
    refl
  7. L30
    trans (((c * g) * (c * g)) + (((a * g) * (a * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))))
  8. L31
    congr
  9. L32
    refl
  10. L33
    trans (((d * h) * (d * h)) + (((a * g) * (a * g)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))
06Calculate and transport equalitiesL34–41

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

  1. L34
    congr
  2. L35
    refl
  3. L36
    trans (((c * h) * (c * h)) + (((a * g) * (a * g)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))
  4. L37
    congr
  5. L38
    refl
  6. L39
    trans (((b * e) * (b * e)) + (((a * g) * (a * g)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))
  7. L40
    congr
  8. L41
    refl
07Use earlier factsL42–47

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

  1. L42
    apply four_square_add_swap_right_tail
  2. L43
    apply four_square_add_swap_right_tail
  3. L44
    apply four_square_add_swap_right_tail
  4. L45
    apply four_square_add_swap_right_tail
  5. L46
    apply four_square_add_swap_right_tail
  6. L47
    apply four_square_add_swap_right_tail
08Calculate and transport equalitiesL48–57

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

  1. L48
    congr
  2. L49
    refl
  3. L50
    trans (((a * h) * (a * h)) + (((b * f) * (b * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))))
  4. L51
    trans (((b * f) * (b * f)) + (((a * h) * (a * h)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))))
  5. L52
    congr
  6. L53
    refl
  7. L54
    trans (((c * g) * (c * g)) + (((a * h) * (a * h)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))
  8. L55
    congr
  9. L56
    refl
  10. L57
    trans (((d * h) * (d * h)) + (((a * h) * (a * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))
09Calculate and transport equalitiesL58–67

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

  1. L58
    congr
  2. L59
    refl
  3. L60
    trans (((c * h) * (c * h)) + (((a * h) * (a * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))
  4. L61
    congr
  5. L62
    refl
  6. L63
    trans (((b * e) * (b * e)) + (((a * h) * (a * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))
  7. L64
    congr
  8. L65
    refl
  9. L66
    trans (((d * g) * (d * g)) + (((a * h) * (a * h)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))
  10. L67
    congr
10Calculate and transport equalitiesL68–74

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

  1. L68
    refl
  2. L69
    trans (((d * f) * (d * f)) + (((a * h) * (a * h)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))
  3. L70
    congr
  4. L71
    refl
  5. L72
    trans (((c * e) * (c * e)) + (((a * h) * (a * h)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))
  6. L73
    congr
  7. L74
    refl
11Use earlier factsL75–83

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

  1. L75
    apply four_square_add_swap_right_tail
  2. L76
    apply four_square_add_swap_right_tail
  3. L77
    apply four_square_add_swap_right_tail
  4. L78
    apply four_square_add_swap_right_tail
  5. L79
    apply four_square_add_swap_right_tail
  6. L80
    apply four_square_add_swap_right_tail
  7. L81
    apply four_square_add_swap_right_tail
  8. L82
    apply four_square_add_swap_right_tail
  9. L83
    apply four_square_add_swap_right_tail
12Calculate and transport equalitiesL84–93

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

  1. L84
    congr
  2. L85
    refl
  3. L86
    trans (((b * e) * (b * e)) + (((b * f) * (b * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))
  4. L87
    trans (((b * f) * (b * f)) + (((b * e) * (b * e)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))
  5. L88
    congr
  6. L89
    refl
  7. L90
    trans (((c * g) * (c * g)) + (((b * e) * (b * e)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))
  8. L91
    congr
  9. L92
    refl
  10. L93
    trans (((d * h) * (d * h)) + (((b * e) * (b * e)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))
13Calculate and transport equalitiesL94–95

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

  1. L94
    congr
  2. L95
    refl
14Use earlier factsL96–99

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

  1. L96
    apply four_square_add_swap_right_tail
  2. L97
    apply four_square_add_swap_right_tail
  3. L98
    apply four_square_add_swap_right_tail
  4. 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) * (b * g)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))
  6. L105
    trans (((c * g) * (c * g)) + (((b * g) * (b * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))
  7. L106
    congr
  8. L107
    refl
  9. L108
    trans (((d * h) * (d * h)) + (((b * g) * (b * g)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))
  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 * h) * (c * h)) + (((b * g) * (b * g)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))
  3. L112
    congr
  4. L113
    refl
  5. L114
    trans (((d * g) * (d * g)) + (((b * g) * (b * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))
  6. L115
    congr
  7. L116
    refl
  8. L117
    trans (((d * f) * (d * f)) + (((b * g) * (b * g)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))
  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) * (c * e)) + (((b * g) * (b * g)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))
  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) * (b * h)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))
  4. L133
    trans (((c * g) * (c * g)) + (((b * h) * (b * h)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))
  5. L134
    congr
  6. L135
    refl
  7. L136
    trans (((d * h) * (d * h)) + (((b * h) * (b * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))
  8. L137
    congr
  9. L138
    refl
  10. L139
    trans (((c * h) * (c * h)) + (((b * h) * (b * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))
20Calculate and transport equalitiesL140–147

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

  1. L140
    congr
  2. L141
    refl
  3. L142
    trans (((d * g) * (d * g)) + (((b * h) * (b * h)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))
  4. L143
    congr
  5. L144
    refl
  6. L145
    trans (((d * f) * (d * f)) + (((b * h) * (b * h)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))
  7. L146
    congr
  8. L147
    refl
21Use earlier factsL148–153

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

  1. L148
    apply four_square_add_swap_right_tail
  2. L149
    apply four_square_add_swap_right_tail
  3. L150
    apply four_square_add_swap_right_tail
  4. L151
    apply four_square_add_swap_right_tail
  5. L152
    apply four_square_add_swap_right_tail
  6. L153
    apply four_square_add_swap_right_tail
22Calculate and transport equalitiesL154–163

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

  1. L154
    congr
  2. L155
    refl
  3. L156
    trans (((c * e) * (c * e)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))
  4. L157
    trans (((c * g) * (c * g)) + (((c * e) * (c * e)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))
  5. L158
    congr
  6. L159
    refl
  7. L160
    trans (((d * h) * (d * h)) + (((c * e) * (c * e)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))
  8. L161
    congr
  9. L162
    refl
  10. L163
    trans (((c * h) * (c * h)) + (((c * e) * (c * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))
23Calculate and transport equalitiesL164–168

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

  1. L164
    congr
  2. L165
    refl
  3. L166
    trans (((d * g) * (d * g)) + (((c * e) * (c * e)) + (((d * f) * (d * f)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))
  4. L167
    congr
  5. L168
    refl
24Use earlier factsL169–173

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

  1. L169
    apply four_square_add_swap_right_tail
  2. L170
    apply four_square_add_swap_right_tail
  3. L171
    apply four_square_add_swap_right_tail
  4. L172
    apply four_square_add_swap_right_tail
  5. L173
    apply four_square_add_swap_right_tail
25Calculate and transport equalitiesL174–183

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

  1. L174
    congr
  2. L175
    refl
  3. L176
    trans (((c * f) * (c * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + ((d * e) * (d * e))))))))
  4. L177
    trans (((c * g) * (c * g)) + (((c * f) * (c * f)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + ((d * e) * (d * e))))))))
  5. L178
    congr
  6. L179
    refl
  7. L180
    trans (((d * h) * (d * h)) + (((c * f) * (c * f)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + ((d * e) * (d * e)))))))
  8. L181
    congr
  9. L182
    refl
  10. L183
    trans (((c * h) * (c * h)) + (((c * f) * (c * f)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + ((d * e) * (d * e))))))
26Calculate and transport equalitiesL184–191

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

  1. L184
    congr
  2. L185
    refl
  3. L186
    trans (((d * g) * (d * g)) + (((c * f) * (c * f)) + (((d * f) * (d * f)) + ((d * e) * (d * e)))))
  4. L187
    congr
  5. L188
    refl
  6. L189
    trans (((d * f) * (d * f)) + (((c * f) * (c * f)) + ((d * e) * (d * e))))
  7. L190
    congr
  8. L191
    refl
27Use earlier factsL192–197

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

  1. L192
    apply add_comm
  2. L193
    apply four_square_add_swap_right_tail
  3. L194
    apply four_square_add_swap_right_tail
  4. L195
    apply four_square_add_swap_right_tail
  5. L196
    apply four_square_add_swap_right_tail
  6. L197
    apply four_square_add_swap_right_tail
28Calculate and transport equalitiesL198–202

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

  1. L198
    congr
  2. L199
    refl
  3. L200
    congr
  4. L201
    refl
  5. L202
    trans (((c * h) * (c * h)) + (((d * h) * (d * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + ((d * e) * (d * e))))))
29Use earlier factsL203–203

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

  1. L203
    apply four_square_add_swap_right_tail
30Calculate and transport equalitiesL204–212

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 * e) * (d * e)) + (((d * h) * (d * h)) + (((d * g) * (d * g)) + ((d * f) * (d * f)))))
  4. L207
    trans (((d * h) * (d * h)) + (((d * e) * (d * e)) + (((d * g) * (d * g)) + ((d * f) * (d * f)))))
  5. L208
    congr
  6. L209
    refl
  7. L210
    trans (((d * g) * (d * g)) + (((d * e) * (d * e)) + ((d * f) * (d * f))))
  8. L211
    congr
  9. L212
    refl
31Use earlier factsL213–215

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

  1. L213
    apply add_comm
  2. L214
    apply four_square_add_swap_right_tail
  3. L215
    apply four_square_add_swap_right_tail
32Calculate and transport equalitiesL216–221

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

  1. L216
    congr
  2. L217
    refl
  3. L218
    trans (((d * f) * (d * f)) + (((d * h) * (d * h)) + ((d * g) * (d * g))))
  4. L219
    trans (((d * h) * (d * h)) + (((d * f) * (d * f)) + ((d * g) * (d * g))))
  5. L220
    congr
  6. L221
    refl
33Use earlier factsL222–223

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

  1. L222
    apply add_comm
  2. L223
    apply four_square_add_swap_right_tail
34Calculate and transport equalitiesL224–226

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

  1. L224
    congr
  2. L225
    refl
  3. L226
    trans (((d * g) * (d * g)) + ((d * h) * (d * h)))
35Use earlier factsL227–227

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

  1. L227
    apply add_comm
36Calculate and transport equalitiesL228–232

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

  1. L228
    congr
  2. L229
    refl
  3. L230
    refl
  4. L231
    symm
  5. L232
    simp [add_assoc]

Library-wide reading audit

Original exact command ledger · 232 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. 0009trans (((a * e) * (a * e)) + (((b * f) * (b * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((a * f) * (a * f)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((a * g) * (a * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))))))
  10. 0010simp [add_assoc]
  11. 0011trans (((a * e) * (a * e)) + (((a * f) * (a * f)) + (((a * g) * (a * g)) + (((a * h) * (a * h)) + (((b * e) * (b * e)) + (((b * f) * (b * f)) + (((b * g) * (b * g)) + (((b * h) * (b * h)) + (((c * e) * (c * e)) + (((c * f) * (c * f)) + (((c * g) * (c * g)) + (((c * h) * (c * h)) + (((d * e) * (d * e)) + (((d * f) * (d * f)) + (((d * g) * (d * g)) + ((d * h) * (d * h)))))))))))))))))
  12. 0012congr
  13. 0013refl
  14. 0014trans (((a * f) * (a * f)) + (((b * f) * (b * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((a * g) * (a * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))))))
  15. 0015trans (((b * f) * (b * f)) + (((a * f) * (a * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((a * g) * (a * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))))))
  16. 0016congr
  17. 0017refl
  18. 0018trans (((c * g) * (c * g)) + (((a * f) * (a * f)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((a * g) * (a * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))))
  19. 0019congr
  20. 0020refl
  21. 0021apply four_square_add_swap_right_tail
  22. 0022apply four_square_add_swap_right_tail
  23. 0023apply four_square_add_swap_right_tail
  24. 0024congr
  25. 0025refl
  26. 0026trans (((a * g) * (a * g)) + (((b * f) * (b * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))))
  27. 0027trans (((b * f) * (b * f)) + (((a * g) * (a * g)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))))
  28. 0028congr
  29. 0029refl
  30. 0030trans (((c * g) * (c * g)) + (((a * g) * (a * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))))
  31. 0031congr
  32. 0032refl
  33. 0033trans (((d * h) * (d * h)) + (((a * g) * (a * g)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))
  34. 0034congr
  35. 0035refl
  36. 0036trans (((c * h) * (c * h)) + (((a * g) * (a * g)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))
  37. 0037congr
  38. 0038refl
  39. 0039trans (((b * e) * (b * e)) + (((a * g) * (a * g)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((a * h) * (a * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))
  40. 0040congr
  41. 0041refl
  42. 0042apply four_square_add_swap_right_tail
  43. 0043apply four_square_add_swap_right_tail
  44. 0044apply four_square_add_swap_right_tail
  45. 0045apply four_square_add_swap_right_tail
  46. 0046apply four_square_add_swap_right_tail
  47. 0047apply four_square_add_swap_right_tail
  48. 0048congr
  49. 0049refl
  50. 0050trans (((a * h) * (a * h)) + (((b * f) * (b * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))))
  51. 0051trans (((b * f) * (b * f)) + (((a * h) * (a * h)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))))
  52. 0052congr
  53. 0053refl
  54. 0054trans (((c * g) * (c * g)) + (((a * h) * (a * h)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))
  55. 0055congr
  56. 0056refl
  57. 0057trans (((d * h) * (d * h)) + (((a * h) * (a * h)) + (((c * h) * (c * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))
  58. 0058congr
  59. 0059refl
  60. 0060trans (((c * h) * (c * h)) + (((a * h) * (a * h)) + (((b * e) * (b * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))
  61. 0061congr
  62. 0062refl
  63. 0063trans (((b * e) * (b * e)) + (((a * h) * (a * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))
  64. 0064congr
  65. 0065refl
  66. 0066trans (((d * g) * (d * g)) + (((a * h) * (a * h)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))
  67. 0067congr
  68. 0068refl
  69. 0069trans (((d * f) * (d * f)) + (((a * h) * (a * h)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))
  70. 0070congr
  71. 0071refl
  72. 0072trans (((c * e) * (c * e)) + (((a * h) * (a * h)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))
  73. 0073congr
  74. 0074refl
  75. 0075apply four_square_add_swap_right_tail
  76. 0076apply four_square_add_swap_right_tail
  77. 0077apply four_square_add_swap_right_tail
  78. 0078apply four_square_add_swap_right_tail
  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. 0084congr
  85. 0085refl
  86. 0086trans (((b * e) * (b * e)) + (((b * f) * (b * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))
  87. 0087trans (((b * f) * (b * f)) + (((b * e) * (b * e)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))))
  88. 0088congr
  89. 0089refl
  90. 0090trans (((c * g) * (c * g)) + (((b * e) * (b * e)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))))
  91. 0091congr
  92. 0092refl
  93. 0093trans (((d * h) * (d * h)) + (((b * e) * (b * e)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((b * g) * (b * g)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))
  94. 0094congr
  95. 0095refl
  96. 0096apply four_square_add_swap_right_tail
  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) * (b * g)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))
  105. 0105trans (((c * g) * (c * g)) + (((b * g) * (b * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))))
  106. 0106congr
  107. 0107refl
  108. 0108trans (((d * h) * (d * h)) + (((b * g) * (b * g)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))
  109. 0109congr
  110. 0110refl
  111. 0111trans (((c * h) * (c * h)) + (((b * g) * (b * g)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))
  112. 0112congr
  113. 0113refl
  114. 0114trans (((d * g) * (d * g)) + (((b * g) * (b * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))
  115. 0115congr
  116. 0116refl
  117. 0117trans (((d * f) * (d * f)) + (((b * g) * (b * g)) + (((c * e) * (c * e)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))
  118. 0118congr
  119. 0119refl
  120. 0120trans (((c * e) * (c * e)) + (((b * g) * (b * g)) + (((b * h) * (b * h)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))
  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) * (b * h)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))
  133. 0133trans (((c * g) * (c * g)) + (((b * h) * (b * h)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))))
  134. 0134congr
  135. 0135refl
  136. 0136trans (((d * h) * (d * h)) + (((b * h) * (b * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))
  137. 0137congr
  138. 0138refl
  139. 0139trans (((c * h) * (c * h)) + (((b * h) * (b * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))
  140. 0140congr
  141. 0141refl
  142. 0142trans (((d * g) * (d * g)) + (((b * h) * (b * h)) + (((d * f) * (d * f)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))
  143. 0143congr
  144. 0144refl
  145. 0145trans (((d * f) * (d * f)) + (((b * h) * (b * h)) + (((c * e) * (c * e)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))
  146. 0146congr
  147. 0147refl
  148. 0148apply four_square_add_swap_right_tail
  149. 0149apply four_square_add_swap_right_tail
  150. 0150apply four_square_add_swap_right_tail
  151. 0151apply four_square_add_swap_right_tail
  152. 0152apply four_square_add_swap_right_tail
  153. 0153apply four_square_add_swap_right_tail
  154. 0154congr
  155. 0155refl
  156. 0156trans (((c * e) * (c * e)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))
  157. 0157trans (((c * g) * (c * g)) + (((c * e) * (c * e)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))))
  158. 0158congr
  159. 0159refl
  160. 0160trans (((d * h) * (d * h)) + (((c * e) * (c * e)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))))
  161. 0161congr
  162. 0162refl
  163. 0163trans (((c * h) * (c * h)) + (((c * e) * (c * e)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + (((d * e) * (d * e)) + ((c * f) * (c * f)))))))
  164. 0164congr
  165. 0165refl
  166. 0166trans (((d * g) * (d * g)) + (((c * e) * (c * e)) + (((d * f) * (d * f)) + (((d * e) * (d * e)) + ((c * f) * (c * f))))))
  167. 0167congr
  168. 0168refl
  169. 0169apply four_square_add_swap_right_tail
  170. 0170apply four_square_add_swap_right_tail
  171. 0171apply four_square_add_swap_right_tail
  172. 0172apply four_square_add_swap_right_tail
  173. 0173apply four_square_add_swap_right_tail
  174. 0174congr
  175. 0175refl
  176. 0176trans (((c * f) * (c * f)) + (((c * g) * (c * g)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + ((d * e) * (d * e))))))))
  177. 0177trans (((c * g) * (c * g)) + (((c * f) * (c * f)) + (((d * h) * (d * h)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + ((d * e) * (d * e))))))))
  178. 0178congr
  179. 0179refl
  180. 0180trans (((d * h) * (d * h)) + (((c * f) * (c * f)) + (((c * h) * (c * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + ((d * e) * (d * e)))))))
  181. 0181congr
  182. 0182refl
  183. 0183trans (((c * h) * (c * h)) + (((c * f) * (c * f)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + ((d * e) * (d * e))))))
  184. 0184congr
  185. 0185refl
  186. 0186trans (((d * g) * (d * g)) + (((c * f) * (c * f)) + (((d * f) * (d * f)) + ((d * e) * (d * e)))))
  187. 0187congr
  188. 0188refl
  189. 0189trans (((d * f) * (d * f)) + (((c * f) * (c * f)) + ((d * e) * (d * e))))
  190. 0190congr
  191. 0191refl
  192. 0192apply add_comm
  193. 0193apply four_square_add_swap_right_tail
  194. 0194apply four_square_add_swap_right_tail
  195. 0195apply four_square_add_swap_right_tail
  196. 0196apply four_square_add_swap_right_tail
  197. 0197apply four_square_add_swap_right_tail
  198. 0198congr
  199. 0199refl
  200. 0200congr
  201. 0201refl
  202. 0202trans (((c * h) * (c * h)) + (((d * h) * (d * h)) + (((d * g) * (d * g)) + (((d * f) * (d * f)) + ((d * e) * (d * e))))))
  203. 0203apply four_square_add_swap_right_tail
  204. 0204congr
  205. 0205refl
  206. 0206trans (((d * e) * (d * e)) + (((d * h) * (d * h)) + (((d * g) * (d * g)) + ((d * f) * (d * f)))))
  207. 0207trans (((d * h) * (d * h)) + (((d * e) * (d * e)) + (((d * g) * (d * g)) + ((d * f) * (d * f)))))
  208. 0208congr
  209. 0209refl
  210. 0210trans (((d * g) * (d * g)) + (((d * e) * (d * e)) + ((d * f) * (d * f))))
  211. 0211congr
  212. 0212refl
  213. 0213apply add_comm
  214. 0214apply four_square_add_swap_right_tail
  215. 0215apply four_square_add_swap_right_tail
  216. 0216congr
  217. 0217refl
  218. 0218trans (((d * f) * (d * f)) + (((d * h) * (d * h)) + ((d * g) * (d * g))))
  219. 0219trans (((d * h) * (d * h)) + (((d * f) * (d * f)) + ((d * g) * (d * g))))
  220. 0220congr
  221. 0221refl
  222. 0222apply add_comm
  223. 0223apply four_square_add_swap_right_tail
  224. 0224congr
  225. 0225refl
  226. 0226trans (((d * g) * (d * g)) + ((d * h) * (d * h)))
  227. 0227apply add_comm
  228. 0228congr
  229. 0229refl
  230. 0230refl
  231. 0231symm
  232. 0232simp [add_assoc]