EI0027

eisenstein_coordinate_norm_conjugate

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

The actual Eisenstein conjugate (a-b)-bω has the same norm as a+bω for all signed representatives.

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 N. (((((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))) + (((((a) * (d))) + (((b) * (c)))))) = ((((((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))) + (((((a) * (c))) + (((b) * (d))))))) + (N))) -> (((((((((((a) + (d))) * (((a) + (d))))) + (((((b) + (c))) * (((b) + (c))))))) + (((((d) * (d))) + (((c) * (c))))))) + (((((((a) + (d))) * (c))) + (((((b) + (c))) * (d)))))) = ((((((((((((a) + (d))) * (((b) + (c))))) + (((((b) + (c))) * (((a) + (d))))))) + (((((d) * (c))) + (((c) * (d))))))) + (((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))))) + (N)))

Constructive proof overview

Generated structural guide

The actual Eisenstein conjugate (a-b)-bω has the same norm as a+bω for all signed representatives.

The unchanged tactic script uses 8 declared prerequisites and contains 410 exact native proof lines.

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

Proof neighborhood

Direct dependencies

EI000A eisenstein_pair_natural_value_transport add_mul Stable theorem; checked-use authorized mul_add Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized add_assoc Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized four_square_add_swap_right_tail Alpha theorem; checked-use authorized

Direct dependents

EI0033 eisenstein_signed_euclidean_division_exists

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

410 script commands · 74 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)
eisenstein pair natural value transport
01Fix variables and assumptionsL1–6

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 N
  6. L6
    intro hnorm
02Use earlier factsL7–13

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

  1. L7
    specialize eisenstein_pair_natural_value_transport ((((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))) + (((((a) * (d))) + (((b) * (c))))))
  2. L8
    specialize eisenstein_pair_natural_value_transport ((((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))) + (((((a) * (c))) + (((b) * (d))))))
  3. L9
    specialize eisenstein_pair_natural_value_transport ((((((((((a) + (d))) * (((a) + (d))))) + (((((b) + (c))) * (((b) + (c))))))) + (((((d) * (d))) + (((c) * (c))))))) + (((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))))
  4. L10
    specialize eisenstein_pair_natural_value_transport ((((((((((a) + (d))) * (((b) + (c))))) + (((((b) + (c))) * (((a) + (d))))))) + (((((d) * (c))) + (((c) * (d))))))) + (((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))))
  5. L11
    specialize eisenstein_pair_natural_value_transport N
  6. L12
    apply eisenstein_pair_natural_value_transport
  7. L13
    exact hnorm
03Calculate and transport equalitiesL14–23

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

  1. L14
    trans ((((a) * (a))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((d) * (b))) + ((((d) * (c))) + ((((b) * (a))) + ((((b) * (d))) + ((((c) * (a))) + ((((c) * (d))) + ((((d) * (c))) + ((((c) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))))))
  2. L15
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  3. L16
    trans ((((a) * (a))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))))))
  4. L17
    congr
  5. L18
    refl
  6. L19
    congr
  7. L20
    refl
  8. L21
    congr
  9. L22
    refl
  10. L23
    congr
04Calculate and transport equalitiesL24–33

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

  1. L24
    refl
  2. L25
    congr
  3. L26
    refl
  4. L27
    congr
  5. L28
    refl
  6. L29
    congr
  7. L30
    refl
  8. L31
    congr
  9. L32
    refl
  10. L33
    congr
05Calculate and transport equalitiesL34–34

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

  1. L34
    trans ((b) * (d))
06Use earlier factsL35–35

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

  1. L35
    apply mul_comm
07Calculate and transport equalitiesL36–40

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

  1. L36
    congr
  2. L37
    refl
  3. L38
    refl
  4. L39
    congr
  5. L40
    trans ((c) * (d))
08Use earlier factsL41–41

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

  1. L41
    apply mul_comm
09Calculate and transport equalitiesL42–46

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

  1. L42
    congr
  2. L43
    refl
  3. L44
    refl
  4. L45
    congr
  5. L46
    trans ((a) * (b))
10Use earlier factsL47–47

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

  1. L47
    apply mul_comm
11Calculate and transport equalitiesL48–54

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
    refl
  4. L51
    congr
  5. L52
    refl
  6. L53
    congr
  7. L54
    trans ((a) * (c))
12Use earlier factsL55–55

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

  1. L55
    apply mul_comm
13Calculate and transport equalitiesL56–62

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

  1. L56
    congr
  2. L57
    refl
  3. L58
    refl
  4. L59
    congr
  5. L60
    refl
  6. L61
    congr
  7. L62
    trans ((c) * (d))
14Use earlier factsL63–63

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

  1. L63
    apply mul_comm
15Calculate and transport equalitiesL64–73

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

  1. L64
    congr
  2. L65
    refl
  3. L66
    refl
  4. L67
    congr
  5. L68
    refl
  6. L69
    congr
  7. L70
    refl
  8. L71
    congr
  9. L72
    refl
  10. L73
    congr
16Calculate and transport equalitiesL74–83

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

  1. L74
    refl
  2. L75
    refl
  3. L76
    trans ((((a) * (a))) + ((((a) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (b))) + ((((b) * (c))) + ((((b) * (c))) + ((((c) * (c))) + ((((d) * (d))) + ((((c) * (c))) + ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((a) * (b))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (c))) + (((b) * (d))))))))))))))))))))))
  4. L77
    congr
  5. L78
    refl
  6. L79
    trans ((((a) * (d))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))))))
  7. L80
    trans ((((b) * (b))) + ((((a) * (d))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))))))
  8. L81
    congr
  9. L82
    refl
  10. L83
    trans ((((c) * (c))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))))
17Calculate and transport equalitiesL84–85

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

  1. L84
    congr
  2. L85
    refl
18Use earlier factsL86–88

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

  1. L86
    apply four_square_add_swap_right_tail
  2. L87
    apply four_square_add_swap_right_tail
  3. L88
    apply four_square_add_swap_right_tail
19Calculate and transport equalitiesL89–98

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

  1. L89
    congr
  2. L90
    refl
  3. L91
    trans ((((a) * (d))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))))
  4. L92
    trans ((((b) * (b))) + ((((a) * (d))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))))
  5. L93
    congr
  6. L94
    refl
  7. L95
    trans ((((c) * (c))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))))
  8. L96
    congr
  9. L97
    refl
  10. L98
    trans ((((d) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))
20Calculate and transport equalitiesL99–108

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

  1. L99
    congr
  2. L100
    refl
  3. L101
    trans ((((b) * (c))) + ((((a) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))
  4. L102
    congr
  5. L103
    refl
  6. L104
    trans ((((a) * (b))) + ((((a) * (d))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))
  7. L105
    congr
  8. L106
    refl
  9. L107
    trans ((((a) * (c))) + ((((a) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))
  10. L108
    congr
21Calculate and transport equalitiesL109–118

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

  1. L109
    refl
  2. L110
    trans ((((b) * (d))) + ((((a) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))
  3. L111
    congr
  4. L112
    refl
  5. L113
    trans ((((c) * (d))) + ((((a) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))
  6. L114
    congr
  7. L115
    refl
  8. L116
    trans ((((a) * (b))) + ((((a) * (d))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))
  9. L117
    congr
  10. L118
    refl
22Calculate and transport equalitiesL119–128

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

  1. L119
    trans ((((b) * (d))) + ((((a) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))
  2. L120
    congr
  3. L121
    refl
  4. L122
    trans ((((a) * (c))) + ((((a) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))
  5. L123
    congr
  6. L124
    refl
  7. L125
    trans ((((c) * (d))) + ((((a) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))
  8. L126
    congr
  9. L127
    refl
  10. L128
    trans ((((c) * (d))) + ((((a) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))
23Calculate and transport equalitiesL129–130

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

  1. L129
    congr
  2. L130
    refl
24Use earlier factsL131–140

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

  1. L131
    apply four_square_add_swap_right_tail
  2. L132
    apply four_square_add_swap_right_tail
  3. L133
    apply four_square_add_swap_right_tail
  4. L134
    apply four_square_add_swap_right_tail
  5. L135
    apply four_square_add_swap_right_tail
  6. L136
    apply four_square_add_swap_right_tail
  7. L137
    apply four_square_add_swap_right_tail
  8. L138
    apply four_square_add_swap_right_tail
  9. L139
    apply four_square_add_swap_right_tail
  10. L140
    apply four_square_add_swap_right_tail
25Use earlier factsL141–144

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

  1. L141
    apply four_square_add_swap_right_tail
  2. L142
    apply four_square_add_swap_right_tail
  3. L143
    apply four_square_add_swap_right_tail
  4. L144
    apply four_square_add_swap_right_tail
26Calculate and transport equalitiesL145–150

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

  1. L145
    congr
  2. L146
    refl
  3. L147
    trans ((((d) * (d))) + ((((b) * (b))) + ((((c) * (c))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))))
  4. L148
    trans ((((b) * (b))) + ((((d) * (d))) + ((((c) * (c))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))))
  5. L149
    congr
  6. L150
    refl
27Use earlier factsL151–152

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

  1. L151
    apply four_square_add_swap_right_tail
  2. L152
    apply four_square_add_swap_right_tail
28Calculate and transport equalitiesL153–157

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

  1. L153
    congr
  2. L154
    refl
  3. L155
    congr
  4. L156
    refl
  5. L157
    trans ((((b) * (c))) + ((((c) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))
29Use earlier factsL158–158

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

  1. L158
    apply four_square_add_swap_right_tail
30Calculate and transport equalitiesL159–168

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

  1. L159
    congr
  2. L160
    refl
  3. L161
    trans ((((b) * (c))) + ((((c) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))))))))))
  4. L162
    trans ((((c) * (c))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))))))))))
  5. L163
    congr
  6. L164
    refl
  7. L165
    trans ((((a) * (b))) + ((((b) * (c))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c)))))))))))))))
  8. L166
    congr
  9. L167
    refl
  10. L168
    trans ((((a) * (c))) + ((((b) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))))))))
31Calculate and transport equalitiesL169–178

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

  1. L169
    congr
  2. L170
    refl
  3. L171
    trans ((((b) * (d))) + ((((b) * (c))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c)))))))))))))
  4. L172
    congr
  5. L173
    refl
  6. L174
    trans ((((c) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))))))
  7. L175
    congr
  8. L176
    refl
  9. L177
    trans ((((a) * (b))) + ((((b) * (c))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c)))))))))))
  10. L178
    congr
32Calculate and transport equalitiesL179–188

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

  1. L179
    refl
  2. L180
    trans ((((b) * (d))) + ((((b) * (c))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))))
  3. L181
    congr
  4. L182
    refl
  5. L183
    trans ((((a) * (c))) + ((((b) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c)))))))))
  6. L184
    congr
  7. L185
    refl
  8. L186
    trans ((((c) * (d))) + ((((b) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))
  9. L187
    congr
  10. L188
    refl
33Calculate and transport equalitiesL189–194

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

  1. L189
    trans ((((c) * (d))) + ((((b) * (c))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c)))))))
  2. L190
    congr
  3. L191
    refl
  4. L192
    trans ((((c) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c))))))
  5. L193
    congr
  6. L194
    refl
34Use earlier factsL195–204

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

  1. L195
    apply four_square_add_swap_right_tail
  2. L196
    apply four_square_add_swap_right_tail
  3. L197
    apply four_square_add_swap_right_tail
  4. L198
    apply four_square_add_swap_right_tail
  5. L199
    apply four_square_add_swap_right_tail
  6. L200
    apply four_square_add_swap_right_tail
  7. L201
    apply four_square_add_swap_right_tail
  8. L202
    apply four_square_add_swap_right_tail
  9. L203
    apply four_square_add_swap_right_tail
  10. L204
    apply four_square_add_swap_right_tail
35Use earlier factsL205–206

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

  1. L205
    apply four_square_add_swap_right_tail
  2. L206
    apply four_square_add_swap_right_tail
36Calculate and transport equalitiesL207–216

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

  1. L207
    congr
  2. L208
    refl
  3. L209
    congr
  4. L210
    refl
  5. L211
    trans ((((d) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c))))))))))))))
  6. L212
    trans ((((a) * (b))) + ((((d) * (d))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c))))))))))))))
  7. L213
    congr
  8. L214
    refl
  9. L215
    trans ((((a) * (c))) + ((((d) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c)))))))))))))
  10. L216
    congr
37Calculate and transport equalitiesL217–226

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

  1. L217
    refl
  2. L218
    trans ((((b) * (d))) + ((((d) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c))))))))))))
  3. L219
    congr
  4. L220
    refl
  5. L221
    trans ((((c) * (d))) + ((((d) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c)))))))))))
  6. L222
    congr
  7. L223
    refl
  8. L224
    trans ((((a) * (b))) + ((((d) * (d))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c))))))))))
  9. L225
    congr
  10. L226
    refl
38Calculate and transport equalitiesL227–236

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

  1. L227
    trans ((((b) * (d))) + ((((d) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c)))))))))
  2. L228
    congr
  3. L229
    refl
  4. L230
    trans ((((a) * (c))) + ((((d) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c))))))))
  5. L231
    congr
  6. L232
    refl
  7. L233
    trans ((((c) * (d))) + ((((d) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c)))))))
  8. L234
    congr
  9. L235
    refl
  10. L236
    trans ((((c) * (d))) + ((((d) * (d))) + ((((c) * (d))) + (((c) * (c))))))
39Calculate and transport equalitiesL237–238

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

  1. L237
    congr
  2. L238
    refl
40Use earlier factsL239–248

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

  1. L239
    apply four_square_add_swap_right_tail
  2. L240
    apply four_square_add_swap_right_tail
  3. L241
    apply four_square_add_swap_right_tail
  4. L242
    apply four_square_add_swap_right_tail
  5. L243
    apply four_square_add_swap_right_tail
  6. L244
    apply four_square_add_swap_right_tail
  7. L245
    apply four_square_add_swap_right_tail
  8. L246
    apply four_square_add_swap_right_tail
  9. L247
    apply four_square_add_swap_right_tail
  10. L248
    apply four_square_add_swap_right_tail
41Calculate and transport equalitiesL249–258

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

  1. L249
    congr
  2. L250
    refl
  3. L251
    trans ((((c) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))))))
  4. L252
    trans ((((a) * (b))) + ((((c) * (c))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))))))
  5. L253
    congr
  6. L254
    refl
  7. L255
    trans ((((a) * (c))) + ((((c) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d))))))))))))
  8. L256
    congr
  9. L257
    refl
  10. L258
    trans ((((b) * (d))) + ((((c) * (c))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))))
42Calculate and transport equalitiesL259–268

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

  1. L259
    congr
  2. L260
    refl
  3. L261
    trans ((((c) * (d))) + ((((c) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d))))))))))
  4. L262
    congr
  5. L263
    refl
  6. L264
    trans ((((a) * (b))) + ((((c) * (c))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))
  7. L265
    congr
  8. L266
    refl
  9. L267
    trans ((((b) * (d))) + ((((c) * (c))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d))))))))
  10. L268
    congr
43Calculate and transport equalitiesL269–278

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

  1. L269
    refl
  2. L270
    trans ((((a) * (c))) + ((((c) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))
  3. L271
    congr
  4. L272
    refl
  5. L273
    trans ((((c) * (d))) + ((((c) * (c))) + ((((c) * (d))) + (((c) * (d))))))
  6. L274
    congr
  7. L275
    refl
  8. L276
    trans ((((c) * (d))) + ((((c) * (c))) + (((c) * (d)))))
  9. L277
    congr
  10. L278
    refl
44Use earlier factsL279–288

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

  1. L279
    apply add_comm
  2. L280
    apply four_square_add_swap_right_tail
  3. L281
    apply four_square_add_swap_right_tail
  4. L282
    apply four_square_add_swap_right_tail
  5. L283
    apply four_square_add_swap_right_tail
  6. L284
    apply four_square_add_swap_right_tail
  7. L285
    apply four_square_add_swap_right_tail
  8. L286
    apply four_square_add_swap_right_tail
  9. L287
    apply four_square_add_swap_right_tail
  10. L288
    apply four_square_add_swap_right_tail
45Calculate and transport equalitiesL289–291

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

  1. L289
    congr
  2. L290
    refl
  3. L291
    trans ((((a) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d))))))))))))
46Use earlier factsL292–292

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

  1. L292
    apply four_square_add_swap_right_tail
47Calculate and transport equalitiesL293–298

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

  1. L293
    congr
  2. L294
    refl
  3. L295
    trans ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))))
  4. L296
    trans ((((a) * (b))) + ((((c) * (d))) + ((((b) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))))
  5. L297
    congr
  6. L298
    refl
48Use earlier factsL299–300

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

  1. L299
    apply four_square_add_swap_right_tail
  2. L300
    apply four_square_add_swap_right_tail
49Calculate and transport equalitiesL301–303

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

  1. L301
    congr
  2. L302
    refl
  3. L303
    trans ((((b) * (d))) + ((((a) * (b))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d))))))))))
50Use earlier factsL304–304

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

  1. L304
    apply four_square_add_swap_right_tail
51Calculate and transport equalitiesL305–314

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

  1. L305
    congr
  2. L306
    refl
  3. L307
    trans ((((c) * (d))) + ((((a) * (b))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))
  4. L308
    trans ((((a) * (b))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))
  5. L309
    congr
  6. L310
    refl
  7. L311
    trans ((((a) * (b))) + ((((c) * (d))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))))
  8. L312
    congr
  9. L313
    refl
  10. L314
    trans ((((b) * (d))) + ((((c) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))
52Calculate and transport equalitiesL315–316

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

  1. L315
    congr
  2. L316
    refl
53Use earlier factsL317–320

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

  1. L317
    apply four_square_add_swap_right_tail
  2. L318
    apply four_square_add_swap_right_tail
  3. L319
    apply four_square_add_swap_right_tail
  4. L320
    apply four_square_add_swap_right_tail
54Calculate and transport equalitiesL321–330

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

  1. L321
    congr
  2. L322
    refl
  3. L323
    congr
  4. L324
    refl
  5. L325
    congr
  6. L326
    refl
  7. L327
    trans ((((c) * (d))) + ((((b) * (d))) + ((((a) * (c))) + (((c) * (d))))))
  8. L328
    trans ((((b) * (d))) + ((((c) * (d))) + ((((a) * (c))) + (((c) * (d))))))
  9. L329
    congr
  10. L330
    refl
55Use earlier factsL331–332

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

  1. L331
    apply four_square_add_swap_right_tail
  2. L332
    apply four_square_add_swap_right_tail
56Calculate and transport equalitiesL333–338

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

  1. L333
    congr
  2. L334
    refl
  3. L335
    trans ((((c) * (d))) + ((((b) * (d))) + (((a) * (c)))))
  4. L336
    trans ((((b) * (d))) + ((((c) * (d))) + (((a) * (c)))))
  5. L337
    congr
  6. L338
    refl
57Use earlier factsL339–340

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

  1. L339
    apply add_comm
  2. L340
    apply four_square_add_swap_right_tail
58Calculate and transport equalitiesL341–343

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

  1. L341
    congr
  2. L342
    refl
  3. L343
    trans ((((a) * (c))) + (((b) * (d))))
59Use earlier factsL344–344

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

  1. L344
    apply add_comm
60Calculate and transport equalitiesL345–354

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

  1. L345
    congr
  2. L346
    refl
  3. L347
    refl
  4. L348
    trans ((((a) * (a))) + ((((a) * (d))) + ((((d) * (a))) + ((((d) * (d))) + ((((b) * (b))) + ((((b) * (c))) + ((((c) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((c) * (c))) + ((((a) * (c))) + ((((d) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (a))) + ((((c) * (d))) + ((((d) * (c))) + ((((a) * (c))) + (((b) * (d))))))))))))))))))))))
  5. L349
    symm
  6. L350
    congr
  7. L351
    refl
  8. L352
    congr
  9. L353
    refl
  10. L354
    congr
61Calculate and transport equalitiesL355–355

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

  1. L355
    trans ((a) * (d))
62Use earlier factsL356–356

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

  1. L356
    apply mul_comm
63Calculate and transport equalitiesL357–366

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

  1. L357
    congr
  2. L358
    refl
  3. L359
    refl
  4. L360
    congr
  5. L361
    refl
  6. L362
    congr
  7. L363
    refl
  8. L364
    congr
  9. L365
    refl
  10. L366
    congr
64Calculate and transport equalitiesL367–367

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

  1. L367
    trans ((b) * (c))
65Use earlier factsL368–368

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

  1. L368
    apply mul_comm
66Calculate and transport equalitiesL369–378

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

  1. L369
    congr
  2. L370
    refl
  3. L371
    refl
  4. L372
    congr
  5. L373
    refl
  6. L374
    congr
  7. L375
    refl
  8. L376
    congr
  9. L377
    refl
  10. L378
    congr
67Calculate and transport equalitiesL379–381

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

  1. L379
    refl
  2. L380
    congr
  3. L381
    trans ((c) * (d))
68Use earlier factsL382–382

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

  1. L382
    apply mul_comm
69Calculate and transport equalitiesL383–392

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

  1. L383
    congr
  2. L384
    refl
  3. L385
    refl
  4. L386
    congr
  5. L387
    refl
  6. L388
    congr
  7. L389
    refl
  8. L390
    congr
  9. L391
    refl
  10. L392
    congr
70Calculate and transport equalitiesL393–393

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

  1. L393
    trans ((a) * (b))
71Use earlier factsL394–394

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

  1. L394
    apply mul_comm
72Calculate and transport equalitiesL395–401

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

  1. L395
    congr
  2. L396
    refl
  3. L397
    refl
  4. L398
    congr
  5. L399
    refl
  6. L400
    congr
  7. L401
    trans ((c) * (d))
73Use earlier factsL402–402

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

  1. L402
    apply mul_comm
74Calculate and transport equalitiesL403–410

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

  1. L403
    congr
  2. L404
    refl
  3. L405
    refl
  4. L406
    congr
  5. L407
    refl
  6. L408
    refl
  7. L409
    symm
  8. L410
    simp [add_mul, mul_add, mul_assoc, add_assoc]

Library-wide reading audit

Original exact command ledger · 410 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro N
  6. 0006intro hnorm
  7. 0007specialize eisenstein_pair_natural_value_transport ((((((((a) * (a))) + (((b) * (b))))) + (((((c) * (c))) + (((d) * (d))))))) + (((((a) * (d))) + (((b) * (c))))))
  8. 0008specialize eisenstein_pair_natural_value_transport ((((((((a) * (b))) + (((b) * (a))))) + (((((c) * (d))) + (((d) * (c))))))) + (((((a) * (c))) + (((b) * (d))))))
  9. 0009specialize eisenstein_pair_natural_value_transport ((((((((((a) + (d))) * (((a) + (d))))) + (((((b) + (c))) * (((b) + (c))))))) + (((((d) * (d))) + (((c) * (c))))))) + (((((((a) + (d))) * (c))) + (((((b) + (c))) * (d))))))
  10. 0010specialize eisenstein_pair_natural_value_transport ((((((((((a) + (d))) * (((b) + (c))))) + (((((b) + (c))) * (((a) + (d))))))) + (((((d) * (c))) + (((c) * (d))))))) + (((((((a) + (d))) * (d))) + (((((b) + (c))) * (c))))))
  11. 0011specialize eisenstein_pair_natural_value_transport N
  12. 0012apply eisenstein_pair_natural_value_transport
  13. 0013exact hnorm
  14. 0014trans ((((a) * (a))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((d) * (b))) + ((((d) * (c))) + ((((b) * (a))) + ((((b) * (d))) + ((((c) * (a))) + ((((c) * (d))) + ((((d) * (c))) + ((((c) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))))))
  15. 0015simp [add_mul, mul_add, mul_assoc, add_assoc]
  16. 0016trans ((((a) * (a))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))))))
  17. 0017congr
  18. 0018refl
  19. 0019congr
  20. 0020refl
  21. 0021congr
  22. 0022refl
  23. 0023congr
  24. 0024refl
  25. 0025congr
  26. 0026refl
  27. 0027congr
  28. 0028refl
  29. 0029congr
  30. 0030refl
  31. 0031congr
  32. 0032refl
  33. 0033congr
  34. 0034trans ((b) * (d))
  35. 0035apply mul_comm
  36. 0036congr
  37. 0037refl
  38. 0038refl
  39. 0039congr
  40. 0040trans ((c) * (d))
  41. 0041apply mul_comm
  42. 0042congr
  43. 0043refl
  44. 0044refl
  45. 0045congr
  46. 0046trans ((a) * (b))
  47. 0047apply mul_comm
  48. 0048congr
  49. 0049refl
  50. 0050refl
  51. 0051congr
  52. 0052refl
  53. 0053congr
  54. 0054trans ((a) * (c))
  55. 0055apply mul_comm
  56. 0056congr
  57. 0057refl
  58. 0058refl
  59. 0059congr
  60. 0060refl
  61. 0061congr
  62. 0062trans ((c) * (d))
  63. 0063apply mul_comm
  64. 0064congr
  65. 0065refl
  66. 0066refl
  67. 0067congr
  68. 0068refl
  69. 0069congr
  70. 0070refl
  71. 0071congr
  72. 0072refl
  73. 0073congr
  74. 0074refl
  75. 0075refl
  76. 0076trans ((((a) * (a))) + ((((a) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (b))) + ((((b) * (c))) + ((((b) * (c))) + ((((c) * (c))) + ((((d) * (d))) + ((((c) * (c))) + ((((a) * (c))) + ((((c) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((a) * (b))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (c))) + (((b) * (d))))))))))))))))))))))
  77. 0077congr
  78. 0078refl
  79. 0079trans ((((a) * (d))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))))))
  80. 0080trans ((((b) * (b))) + ((((a) * (d))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))))))
  81. 0081congr
  82. 0082refl
  83. 0083trans ((((c) * (c))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))))
  84. 0084congr
  85. 0085refl
  86. 0086apply four_square_add_swap_right_tail
  87. 0087apply four_square_add_swap_right_tail
  88. 0088apply four_square_add_swap_right_tail
  89. 0089congr
  90. 0090refl
  91. 0091trans ((((a) * (d))) + ((((b) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))))
  92. 0092trans ((((b) * (b))) + ((((a) * (d))) + ((((c) * (c))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))))
  93. 0093congr
  94. 0094refl
  95. 0095trans ((((c) * (c))) + ((((a) * (d))) + ((((d) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))))
  96. 0096congr
  97. 0097refl
  98. 0098trans ((((d) * (d))) + ((((a) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))))
  99. 0099congr
  100. 0100refl
  101. 0101trans ((((b) * (c))) + ((((a) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))
  102. 0102congr
  103. 0103refl
  104. 0104trans ((((a) * (b))) + ((((a) * (d))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))))
  105. 0105congr
  106. 0106refl
  107. 0107trans ((((a) * (c))) + ((((a) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))
  108. 0108congr
  109. 0109refl
  110. 0110trans ((((b) * (d))) + ((((a) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))))
  111. 0111congr
  112. 0112refl
  113. 0113trans ((((c) * (d))) + ((((a) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))
  114. 0114congr
  115. 0115refl
  116. 0116trans ((((a) * (b))) + ((((a) * (d))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))))
  117. 0117congr
  118. 0118refl
  119. 0119trans ((((b) * (d))) + ((((a) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))
  120. 0120congr
  121. 0121refl
  122. 0122trans ((((a) * (c))) + ((((a) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))))
  123. 0123congr
  124. 0124refl
  125. 0125trans ((((c) * (d))) + ((((a) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))
  126. 0126congr
  127. 0127refl
  128. 0128trans ((((c) * (d))) + ((((a) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c))))))))
  129. 0129congr
  130. 0130refl
  131. 0131apply four_square_add_swap_right_tail
  132. 0132apply four_square_add_swap_right_tail
  133. 0133apply four_square_add_swap_right_tail
  134. 0134apply four_square_add_swap_right_tail
  135. 0135apply four_square_add_swap_right_tail
  136. 0136apply four_square_add_swap_right_tail
  137. 0137apply four_square_add_swap_right_tail
  138. 0138apply four_square_add_swap_right_tail
  139. 0139apply four_square_add_swap_right_tail
  140. 0140apply four_square_add_swap_right_tail
  141. 0141apply four_square_add_swap_right_tail
  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. 0145congr
  146. 0146refl
  147. 0147trans ((((d) * (d))) + ((((b) * (b))) + ((((c) * (c))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))))
  148. 0148trans ((((b) * (b))) + ((((d) * (d))) + ((((c) * (c))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))))
  149. 0149congr
  150. 0150refl
  151. 0151apply four_square_add_swap_right_tail
  152. 0152apply four_square_add_swap_right_tail
  153. 0153congr
  154. 0154refl
  155. 0155congr
  156. 0156refl
  157. 0157trans ((((b) * (c))) + ((((c) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + ((((b) * (c))) + (((c) * (c)))))))))))))))))
  158. 0158apply four_square_add_swap_right_tail
  159. 0159congr
  160. 0160refl
  161. 0161trans ((((b) * (c))) + ((((c) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))))))))))
  162. 0162trans ((((c) * (c))) + ((((b) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))))))))))
  163. 0163congr
  164. 0164refl
  165. 0165trans ((((a) * (b))) + ((((b) * (c))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c)))))))))))))))
  166. 0166congr
  167. 0167refl
  168. 0168trans ((((a) * (c))) + ((((b) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))))))))
  169. 0169congr
  170. 0170refl
  171. 0171trans ((((b) * (d))) + ((((b) * (c))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c)))))))))))))
  172. 0172congr
  173. 0173refl
  174. 0174trans ((((c) * (d))) + ((((b) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))))))
  175. 0175congr
  176. 0176refl
  177. 0177trans ((((a) * (b))) + ((((b) * (c))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c)))))))))))
  178. 0178congr
  179. 0179refl
  180. 0180trans ((((b) * (d))) + ((((b) * (c))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))))
  181. 0181congr
  182. 0182refl
  183. 0183trans ((((a) * (c))) + ((((b) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c)))))))))
  184. 0184congr
  185. 0185refl
  186. 0186trans ((((c) * (d))) + ((((b) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c))))))))
  187. 0187congr
  188. 0188refl
  189. 0189trans ((((c) * (d))) + ((((b) * (c))) + ((((c) * (d))) + ((((d) * (d))) + (((c) * (c)))))))
  190. 0190congr
  191. 0191refl
  192. 0192trans ((((c) * (d))) + ((((b) * (c))) + ((((d) * (d))) + (((c) * (c))))))
  193. 0193congr
  194. 0194refl
  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. 0198apply four_square_add_swap_right_tail
  199. 0199apply four_square_add_swap_right_tail
  200. 0200apply four_square_add_swap_right_tail
  201. 0201apply four_square_add_swap_right_tail
  202. 0202apply four_square_add_swap_right_tail
  203. 0203apply four_square_add_swap_right_tail
  204. 0204apply four_square_add_swap_right_tail
  205. 0205apply four_square_add_swap_right_tail
  206. 0206apply four_square_add_swap_right_tail
  207. 0207congr
  208. 0208refl
  209. 0209congr
  210. 0210refl
  211. 0211trans ((((d) * (d))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c))))))))))))))
  212. 0212trans ((((a) * (b))) + ((((d) * (d))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c))))))))))))))
  213. 0213congr
  214. 0214refl
  215. 0215trans ((((a) * (c))) + ((((d) * (d))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c)))))))))))))
  216. 0216congr
  217. 0217refl
  218. 0218trans ((((b) * (d))) + ((((d) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c))))))))))))
  219. 0219congr
  220. 0220refl
  221. 0221trans ((((c) * (d))) + ((((d) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c)))))))))))
  222. 0222congr
  223. 0223refl
  224. 0224trans ((((a) * (b))) + ((((d) * (d))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c))))))))))
  225. 0225congr
  226. 0226refl
  227. 0227trans ((((b) * (d))) + ((((d) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c)))))))))
  228. 0228congr
  229. 0229refl
  230. 0230trans ((((a) * (c))) + ((((d) * (d))) + ((((c) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c))))))))
  231. 0231congr
  232. 0232refl
  233. 0233trans ((((c) * (d))) + ((((d) * (d))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (c)))))))
  234. 0234congr
  235. 0235refl
  236. 0236trans ((((c) * (d))) + ((((d) * (d))) + ((((c) * (d))) + (((c) * (c))))))
  237. 0237congr
  238. 0238refl
  239. 0239apply four_square_add_swap_right_tail
  240. 0240apply four_square_add_swap_right_tail
  241. 0241apply four_square_add_swap_right_tail
  242. 0242apply four_square_add_swap_right_tail
  243. 0243apply four_square_add_swap_right_tail
  244. 0244apply four_square_add_swap_right_tail
  245. 0245apply four_square_add_swap_right_tail
  246. 0246apply four_square_add_swap_right_tail
  247. 0247apply four_square_add_swap_right_tail
  248. 0248apply four_square_add_swap_right_tail
  249. 0249congr
  250. 0250refl
  251. 0251trans ((((c) * (c))) + ((((a) * (b))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))))))
  252. 0252trans ((((a) * (b))) + ((((c) * (c))) + ((((a) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))))))
  253. 0253congr
  254. 0254refl
  255. 0255trans ((((a) * (c))) + ((((c) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d))))))))))))
  256. 0256congr
  257. 0257refl
  258. 0258trans ((((b) * (d))) + ((((c) * (c))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))))
  259. 0259congr
  260. 0260refl
  261. 0261trans ((((c) * (d))) + ((((c) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d))))))))))
  262. 0262congr
  263. 0263refl
  264. 0264trans ((((a) * (b))) + ((((c) * (c))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))
  265. 0265congr
  266. 0266refl
  267. 0267trans ((((b) * (d))) + ((((c) * (c))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d))))))))
  268. 0268congr
  269. 0269refl
  270. 0270trans ((((a) * (c))) + ((((c) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))
  271. 0271congr
  272. 0272refl
  273. 0273trans ((((c) * (d))) + ((((c) * (c))) + ((((c) * (d))) + (((c) * (d))))))
  274. 0274congr
  275. 0275refl
  276. 0276trans ((((c) * (d))) + ((((c) * (c))) + (((c) * (d)))))
  277. 0277congr
  278. 0278refl
  279. 0279apply add_comm
  280. 0280apply four_square_add_swap_right_tail
  281. 0281apply four_square_add_swap_right_tail
  282. 0282apply four_square_add_swap_right_tail
  283. 0283apply four_square_add_swap_right_tail
  284. 0284apply four_square_add_swap_right_tail
  285. 0285apply four_square_add_swap_right_tail
  286. 0286apply four_square_add_swap_right_tail
  287. 0287apply four_square_add_swap_right_tail
  288. 0288apply four_square_add_swap_right_tail
  289. 0289congr
  290. 0290refl
  291. 0291trans ((((a) * (c))) + ((((a) * (b))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d))))))))))))
  292. 0292apply four_square_add_swap_right_tail
  293. 0293congr
  294. 0294refl
  295. 0295trans ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))))
  296. 0296trans ((((a) * (b))) + ((((c) * (d))) + ((((b) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d)))))))))))
  297. 0297congr
  298. 0298refl
  299. 0299apply four_square_add_swap_right_tail
  300. 0300apply four_square_add_swap_right_tail
  301. 0301congr
  302. 0302refl
  303. 0303trans ((((b) * (d))) + ((((a) * (b))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + ((((c) * (d))) + (((c) * (d))))))))))
  304. 0304apply four_square_add_swap_right_tail
  305. 0305congr
  306. 0306refl
  307. 0307trans ((((c) * (d))) + ((((a) * (b))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))
  308. 0308trans ((((a) * (b))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))))
  309. 0309congr
  310. 0310refl
  311. 0311trans ((((a) * (b))) + ((((c) * (d))) + ((((b) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d))))))))
  312. 0312congr
  313. 0313refl
  314. 0314trans ((((b) * (d))) + ((((c) * (d))) + ((((a) * (c))) + ((((c) * (d))) + (((c) * (d)))))))
  315. 0315congr
  316. 0316refl
  317. 0317apply four_square_add_swap_right_tail
  318. 0318apply four_square_add_swap_right_tail
  319. 0319apply four_square_add_swap_right_tail
  320. 0320apply four_square_add_swap_right_tail
  321. 0321congr
  322. 0322refl
  323. 0323congr
  324. 0324refl
  325. 0325congr
  326. 0326refl
  327. 0327trans ((((c) * (d))) + ((((b) * (d))) + ((((a) * (c))) + (((c) * (d))))))
  328. 0328trans ((((b) * (d))) + ((((c) * (d))) + ((((a) * (c))) + (((c) * (d))))))
  329. 0329congr
  330. 0330refl
  331. 0331apply four_square_add_swap_right_tail
  332. 0332apply four_square_add_swap_right_tail
  333. 0333congr
  334. 0334refl
  335. 0335trans ((((c) * (d))) + ((((b) * (d))) + (((a) * (c)))))
  336. 0336trans ((((b) * (d))) + ((((c) * (d))) + (((a) * (c)))))
  337. 0337congr
  338. 0338refl
  339. 0339apply add_comm
  340. 0340apply four_square_add_swap_right_tail
  341. 0341congr
  342. 0342refl
  343. 0343trans ((((a) * (c))) + (((b) * (d))))
  344. 0344apply add_comm
  345. 0345congr
  346. 0346refl
  347. 0347refl
  348. 0348trans ((((a) * (a))) + ((((a) * (d))) + ((((d) * (a))) + ((((d) * (d))) + ((((b) * (b))) + ((((b) * (c))) + ((((c) * (b))) + ((((c) * (c))) + ((((d) * (d))) + ((((c) * (c))) + ((((a) * (c))) + ((((d) * (c))) + ((((b) * (d))) + ((((c) * (d))) + ((((a) * (b))) + ((((b) * (a))) + ((((c) * (d))) + ((((d) * (c))) + ((((a) * (c))) + (((b) * (d))))))))))))))))))))))
  349. 0349symm
  350. 0350congr
  351. 0351refl
  352. 0352congr
  353. 0353refl
  354. 0354congr
  355. 0355trans ((a) * (d))
  356. 0356apply mul_comm
  357. 0357congr
  358. 0358refl
  359. 0359refl
  360. 0360congr
  361. 0361refl
  362. 0362congr
  363. 0363refl
  364. 0364congr
  365. 0365refl
  366. 0366congr
  367. 0367trans ((b) * (c))
  368. 0368apply mul_comm
  369. 0369congr
  370. 0370refl
  371. 0371refl
  372. 0372congr
  373. 0373refl
  374. 0374congr
  375. 0375refl
  376. 0376congr
  377. 0377refl
  378. 0378congr
  379. 0379refl
  380. 0380congr
  381. 0381trans ((c) * (d))
  382. 0382apply mul_comm
  383. 0383congr
  384. 0384refl
  385. 0385refl
  386. 0386congr
  387. 0387refl
  388. 0388congr
  389. 0389refl
  390. 0390congr
  391. 0391refl
  392. 0392congr
  393. 0393trans ((a) * (b))
  394. 0394apply mul_comm
  395. 0395congr
  396. 0396refl
  397. 0397refl
  398. 0398congr
  399. 0399refl
  400. 0400congr
  401. 0401trans ((c) * (d))
  402. 0402apply mul_comm
  403. 0403congr
  404. 0404refl
  405. 0405refl
  406. 0406congr
  407. 0407refl
  408. 0408refl
  409. 0409symm
  410. 0410simp [add_mul, mul_add, mul_assoc, add_assoc]