GI000B

gaussian_signed_product_square_negative

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

The negative square block of an actual signed product expands into the two negative convolution blocks.

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 p n q m. ((((((((p) * (q))) + (((n) * (m))))) * (((((p) * (m))) + (((n) * (q))))))) + (((((((p) * (m))) + (((n) * (q))))) * (((((p) * (q))) + (((n) * (m)))))))) = ((((((((p) * (p))) + (((n) * (n))))) * (((((q) * (m))) + (((m) * (q))))))) + (((((((p) * (n))) + (((n) * (p))))) * (((((q) * (q))) + (((m) * (m))))))))

Constructive proof overview

Generated structural guide

The negative square block of an actual signed product expands into the two negative convolution blocks.

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

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

Proof neighborhood

Direct dependencies

add_mul Stable theorem; checked-use authorized mul_add Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized add_assoc Stable theorem; checked-use authorized add_comm Stable theorem; checked-use authorized four_square_add_swap_right_tail Alpha theorem; checked-use authorized GI0001 natural_mul_swap_right_tail

Direct dependents

GI000D gaussian_signed_square_product

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

255 script commands · 61 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)
natural mul swap right tail
01Fix variables and assumptionsL1–4

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro q
  4. L4
    intro m
02Calculate and transport equalitiesL5–14

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

  1. L5
    trans ((((p) * (((q) * (((p) * (m))))))) + ((((p) * (((q) * (((n) * (q))))))) + ((((n) * (((m) * (((p) * (m))))))) + ((((n) * (((m) * (((n) * (q))))))) + ((((p) * (((m) * (((p) * (q))))))) + ((((p) * (((m) * (((n) * (m))))))) + ((((n) * (((q) * (((p) * (q))))))) + (((n) * (((q) * (((n) * (m))))))))))))))
  2. L6
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  3. L7
    trans ((((m) * (((p) * (((p) * (q))))))) + ((((n) * (((p) * (((q) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((m) * (((n) * (((n) * (q))))))) + ((((m) * (((p) * (((p) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((n) * (((p) * (((q) * (q))))))) + (((m) * (((n) * (((n) * (q))))))))))))))
  4. L8
    congr
  5. L9
    trans ((m) * (((p) * (((q) * (p))))))
  6. L10
    trans ((p) * (((m) * (((q) * (p))))))
  7. L11
    congr
  8. L12
    refl
  9. L13
    trans ((q) * (((m) * (p))))
  10. L14
    congr
03Calculate and transport equalitiesL15–15

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

  1. L15
    refl
04Use earlier factsL16–18

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

  1. L16
    apply mul_comm
  2. L17
    apply natural_mul_swap_right_tail
  3. L18
    apply natural_mul_swap_right_tail
05Calculate and transport equalitiesL19–23

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

  1. L19
    congr
  2. L20
    refl
  3. L21
    congr
  4. L22
    refl
  5. L23
    trans ((p) * (q))
06Use earlier factsL24–24

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

  1. L24
    apply mul_comm
07Calculate and transport equalitiesL25–32

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

  1. L25
    congr
  2. L26
    refl
  3. L27
    refl
  4. L28
    congr
  5. L29
    trans ((n) * (((p) * (((q) * (q))))))
  6. L30
    trans ((p) * (((n) * (((q) * (q))))))
  7. L31
    congr
  8. L32
    refl
08Use earlier factsL33–34

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

  1. L33
    apply natural_mul_swap_right_tail
  2. L34
    apply natural_mul_swap_right_tail
09Calculate and transport equalitiesL35–39

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

  1. L35
    congr
  2. L36
    refl
  3. L37
    refl
  4. L38
    congr
  5. L39
    trans ((m) * (((n) * (((p) * (m))))))
10Use earlier factsL40–40

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

  1. L40
    apply natural_mul_swap_right_tail
11Calculate and transport equalitiesL41–46

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

  1. L41
    congr
  2. L42
    refl
  3. L43
    trans ((m) * (((n) * (p))))
  4. L44
    trans ((n) * (((m) * (p))))
  5. L45
    congr
  6. L46
    refl
12Use earlier factsL47–48

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

  1. L47
    apply mul_comm
  2. L48
    apply natural_mul_swap_right_tail
13Calculate and transport equalitiesL49–53

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

  1. L49
    congr
  2. L50
    refl
  3. L51
    refl
  4. L52
    congr
  5. L53
    trans ((m) * (((n) * (((n) * (q))))))
14Use earlier factsL54–54

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

  1. L54
    apply natural_mul_swap_right_tail
15Calculate and transport equalitiesL55–59

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

  1. L55
    congr
  2. L56
    refl
  3. L57
    refl
  4. L58
    congr
  5. L59
    trans ((m) * (((p) * (((p) * (q))))))
16Use earlier factsL60–60

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

  1. L60
    apply natural_mul_swap_right_tail
17Calculate and transport equalitiesL61–65

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

  1. L61
    congr
  2. L62
    refl
  3. L63
    refl
  4. L64
    congr
  5. L65
    trans ((m) * (((p) * (((n) * (m))))))
18Use earlier factsL66–66

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

  1. L66
    apply natural_mul_swap_right_tail
19Calculate and transport equalitiesL67–72

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

  1. L67
    congr
  2. L68
    refl
  3. L69
    trans ((m) * (((p) * (n))))
  4. L70
    trans ((p) * (((m) * (n))))
  5. L71
    congr
  6. L72
    refl
20Use earlier factsL73–74

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

  1. L73
    apply mul_comm
  2. L74
    apply natural_mul_swap_right_tail
21Calculate and transport equalitiesL75–77

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

  1. L75
    congr
  2. L76
    refl
  3. L77
    trans ((n) * (p))
22Use earlier factsL78–78

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

  1. L78
    apply mul_comm
23Calculate and transport equalitiesL79–85

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

  1. L79
    congr
  2. L80
    refl
  3. L81
    refl
  4. L82
    congr
  5. L83
    congr
  6. L84
    refl
  7. L85
    trans ((p) * (((q) * (q))))
24Use earlier factsL86–86

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

  1. L86
    apply natural_mul_swap_right_tail
25Calculate and transport equalitiesL87–96

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

  1. L87
    congr
  2. L88
    refl
  3. L89
    refl
  4. L90
    trans ((m) * (((n) * (((q) * (n))))))
  5. L91
    trans ((n) * (((m) * (((q) * (n))))))
  6. L92
    congr
  7. L93
    refl
  8. L94
    trans ((q) * (((m) * (n))))
  9. L95
    congr
  10. L96
    refl
26Use earlier factsL97–99

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

  1. L97
    apply mul_comm
  2. L98
    apply natural_mul_swap_right_tail
  3. L99
    apply natural_mul_swap_right_tail
27Calculate and transport equalitiesL100–104

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 ((n) * (q))
28Use earlier factsL105–105

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

  1. L105
    apply mul_comm
29Calculate and transport equalitiesL106–115

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

  1. L106
    congr
  2. L107
    refl
  3. L108
    refl
  4. L109
    trans ((((m) * (((p) * (((p) * (q))))))) + ((((m) * (((p) * (((p) * (q))))))) + ((((m) * (((n) * (((n) * (q))))))) + ((((m) * (((n) * (((n) * (q))))))) + ((((n) * (((p) * (((q) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((n) * (((p) * (((q) * (q))))))) + (((m) * (((m) * (((n) * (p))))))))))))))
  5. L110
    congr
  6. L111
    refl
  7. L112
    trans ((((m) * (((p) * (((p) * (q))))))) + ((((n) * (((p) * (((q) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((m) * (((n) * (((n) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((n) * (((p) * (((q) * (q))))))) + (((m) * (((n) * (((n) * (q)))))))))))))
  8. L113
    trans ((((n) * (((p) * (((q) * (q))))))) + ((((m) * (((p) * (((p) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((m) * (((n) * (((n) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((n) * (((p) * (((q) * (q))))))) + (((m) * (((n) * (((n) * (q)))))))))))))
  9. L114
    congr
  10. L115
    refl
30Calculate and transport equalitiesL116–118

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

  1. L116
    trans ((((m) * (((m) * (((n) * (p))))))) + ((((m) * (((p) * (((p) * (q))))))) + ((((m) * (((n) * (((n) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((n) * (((p) * (((q) * (q))))))) + (((m) * (((n) * (((n) * (q))))))))))))
  2. L117
    congr
  3. L118
    refl
31Use earlier factsL119–121

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

  1. L119
    apply four_square_add_swap_right_tail
  2. L120
    apply four_square_add_swap_right_tail
  3. L121
    apply four_square_add_swap_right_tail
32Calculate and transport equalitiesL122–127

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

  1. L122
    congr
  2. L123
    refl
  3. L124
    trans ((((m) * (((n) * (((n) * (q))))))) + ((((n) * (((p) * (((q) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((n) * (((p) * (((q) * (q))))))) + (((m) * (((n) * (((n) * (q))))))))))))
  4. L125
    trans ((((n) * (((p) * (((q) * (q))))))) + ((((m) * (((n) * (((n) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((n) * (((p) * (((q) * (q))))))) + (((m) * (((n) * (((n) * (q))))))))))))
  5. L126
    congr
  6. L127
    refl
33Use earlier factsL128–129

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

  1. L128
    apply four_square_add_swap_right_tail
  2. L129
    apply four_square_add_swap_right_tail
34Calculate 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 ((((m) * (((n) * (((n) * (q))))))) + ((((n) * (((p) * (((q) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((m) * (((m) * (((n) * (p))))))) + (((n) * (((p) * (((q) * (q)))))))))))
  4. L133
    trans ((((n) * (((p) * (((q) * (q))))))) + ((((m) * (((n) * (((n) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + ((((m) * (((m) * (((n) * (p))))))) + (((n) * (((p) * (((q) * (q)))))))))))
  5. L134
    congr
  6. L135
    refl
  7. L136
    trans ((((m) * (((m) * (((n) * (p))))))) + ((((m) * (((n) * (((n) * (q))))))) + ((((m) * (((m) * (((n) * (p))))))) + (((n) * (((p) * (((q) * (q))))))))))
  8. L137
    congr
  9. L138
    refl
  10. L139
    trans ((((m) * (((m) * (((n) * (p))))))) + ((((m) * (((n) * (((n) * (q))))))) + (((n) * (((p) * (((q) * (q)))))))))
35Calculate and transport equalitiesL140–141

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

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

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

  1. L142
    apply add_comm
  2. L143
    apply four_square_add_swap_right_tail
  3. L144
    apply four_square_add_swap_right_tail
  4. L145
    apply four_square_add_swap_right_tail
37Calculate and transport equalitiesL146–152

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

  1. L146
    congr
  2. L147
    refl
  3. L148
    congr
  4. L149
    refl
  5. L150
    congr
  6. L151
    refl
  7. L152
    trans ((((n) * (((p) * (((q) * (q))))))) + (((m) * (((m) * (((n) * (p))))))))
38Use earlier factsL153–153

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

  1. L153
    apply add_comm
39Calculate 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
    refl
  4. L157
    trans ((((p) * (((p) * (((q) * (m))))))) + ((((p) * (((p) * (((m) * (q))))))) + ((((n) * (((n) * (((q) * (m))))))) + ((((n) * (((n) * (((m) * (q))))))) + ((((p) * (((n) * (((q) * (q))))))) + ((((p) * (((n) * (((m) * (m))))))) + ((((n) * (((p) * (((q) * (q))))))) + (((n) * (((p) * (((m) * (m))))))))))))))
  5. L158
    symm
  6. L159
    congr
  7. L160
    trans ((m) * (((p) * (((p) * (q))))))
  8. L161
    trans ((p) * (((m) * (((p) * (q))))))
  9. L162
    congr
  10. L163
    refl
40Calculate and transport equalitiesL164–166

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

  1. L164
    trans ((p) * (((m) * (q))))
  2. L165
    congr
  3. L166
    refl
41Use earlier factsL167–169

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

  1. L167
    apply mul_comm
  2. L168
    apply natural_mul_swap_right_tail
  3. L169
    apply natural_mul_swap_right_tail
42Calculate and transport equalitiesL170–177

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

  1. L170
    congr
  2. L171
    refl
  3. L172
    refl
  4. L173
    congr
  5. L174
    trans ((m) * (((p) * (((p) * (q))))))
  6. L175
    trans ((p) * (((m) * (((p) * (q))))))
  7. L176
    congr
  8. L177
    refl
43Use earlier factsL178–179

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

  1. L178
    apply natural_mul_swap_right_tail
  2. L179
    apply natural_mul_swap_right_tail
44Calculate and transport equalitiesL180–189

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

  1. L180
    congr
  2. L181
    refl
  3. L182
    refl
  4. L183
    congr
  5. L184
    trans ((m) * (((n) * (((n) * (q))))))
  6. L185
    trans ((n) * (((m) * (((n) * (q))))))
  7. L186
    congr
  8. L187
    refl
  9. L188
    trans ((n) * (((m) * (q))))
  10. L189
    congr
45Calculate and transport equalitiesL190–190

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

  1. L190
    refl
46Use earlier factsL191–193

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

  1. L191
    apply mul_comm
  2. L192
    apply natural_mul_swap_right_tail
  3. L193
    apply natural_mul_swap_right_tail
47Calculate and transport equalitiesL194–201

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

  1. L194
    congr
  2. L195
    refl
  3. L196
    refl
  4. L197
    congr
  5. L198
    trans ((m) * (((n) * (((n) * (q))))))
  6. L199
    trans ((n) * (((m) * (((n) * (q))))))
  7. L200
    congr
  8. L201
    refl
48Use earlier factsL202–203

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

  1. L202
    apply natural_mul_swap_right_tail
  2. L203
    apply natural_mul_swap_right_tail
49Calculate and transport equalitiesL204–208

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
    refl
  4. L207
    congr
  5. L208
    trans ((n) * (((p) * (((q) * (q))))))
50Use earlier factsL209–209

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

  1. L209
    apply natural_mul_swap_right_tail
51Calculate and transport equalitiesL210–217

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

  1. L210
    congr
  2. L211
    refl
  3. L212
    refl
  4. L213
    congr
  5. L214
    trans ((m) * (((p) * (((n) * (m))))))
  6. L215
    trans ((p) * (((m) * (((n) * (m))))))
  7. L216
    congr
  8. L217
    refl
52Use earlier factsL218–219

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

  1. L218
    apply natural_mul_swap_right_tail
  2. L219
    apply natural_mul_swap_right_tail
53Calculate and transport equalitiesL220–225

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

  1. L220
    congr
  2. L221
    refl
  3. L222
    trans ((m) * (((p) * (n))))
  4. L223
    trans ((p) * (((m) * (n))))
  5. L224
    congr
  6. L225
    refl
54Use earlier factsL226–227

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

  1. L226
    apply mul_comm
  2. L227
    apply natural_mul_swap_right_tail
55Calculate and transport equalitiesL228–230

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
    trans ((n) * (p))
56Use earlier factsL231–231

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

  1. L231
    apply mul_comm
57Calculate and transport equalitiesL232–240

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

  1. L232
    congr
  2. L233
    refl
  3. L234
    refl
  4. L235
    congr
  5. L236
    refl
  6. L237
    trans ((m) * (((n) * (((p) * (m))))))
  7. L238
    trans ((n) * (((m) * (((p) * (m))))))
  8. L239
    congr
  9. L240
    refl
58Use earlier factsL241–242

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

  1. L241
    apply natural_mul_swap_right_tail
  2. L242
    apply natural_mul_swap_right_tail
59Calculate and transport equalitiesL243–248

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

  1. L243
    congr
  2. L244
    refl
  3. L245
    trans ((m) * (((n) * (p))))
  4. L246
    trans ((n) * (((m) * (p))))
  5. L247
    congr
  6. L248
    refl
60Use earlier factsL249–250

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

  1. L249
    apply mul_comm
  2. L250
    apply natural_mul_swap_right_tail
61Calculate and transport equalitiesL251–255

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

  1. L251
    congr
  2. L252
    refl
  3. L253
    refl
  4. L254
    symm
  5. L255
    simp [add_mul, mul_add, mul_assoc, add_assoc]

Library-wide reading audit

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