GI000A

gaussian_signed_product_square_positive

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

The positive square block of an actual signed product expands into its two positive 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) * (q))) + (((n) * (m))))))) + (((((((p) * (m))) + (((n) * (q))))) * (((((p) * (m))) + (((n) * (q)))))))) = ((((((((p) * (p))) + (((n) * (n))))) * (((((q) * (q))) + (((m) * (m))))))) + (((((((p) * (n))) + (((n) * (p))))) * (((((q) * (m))) + (((m) * (q))))))))

Constructive proof overview

Generated structural guide

The positive square block of an actual signed product expands into its two positive convolution blocks.

The unchanged tactic script uses 8 declared prerequisites and contains 251 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

251 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–11

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

  1. L5
    trans ((((p) * (((q) * (((p) * (q))))))) + ((((p) * (((q) * (((n) * (m))))))) + ((((n) * (((m) * (((p) * (q))))))) + ((((n) * (((m) * (((n) * (m))))))) + ((((p) * (((m) * (((p) * (m))))))) + ((((p) * (((m) * (((n) * (q))))))) + ((((n) * (((q) * (((p) * (m))))))) + (((n) * (((q) * (((n) * (q))))))))))))))
  2. L6
    simp [add_mul, mul_add, mul_assoc, add_assoc]
  3. L7
    trans ((((p) * (((p) * (((q) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((m) * (((n) * (n))))))) + ((((m) * (((m) * (((p) * (p))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((n) * (((n) * (((q) * (q))))))))))))))
  4. L8
    congr
  5. L9
    congr
  6. L10
    refl
  7. L11
    trans ((p) * (((q) * (q))))
03Use earlier factsL12–12

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

  1. L12
    apply natural_mul_swap_right_tail
04Calculate and transport equalitiesL13–22

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

  1. L13
    congr
  2. L14
    refl
  3. L15
    refl
  4. L16
    congr
  5. L17
    trans ((m) * (((p) * (((q) * (n))))))
  6. L18
    trans ((p) * (((m) * (((q) * (n))))))
  7. L19
    congr
  8. L20
    refl
  9. L21
    trans ((q) * (((m) * (n))))
  10. L22
    congr
05Calculate and transport equalitiesL23–23

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

  1. L23
    refl
06Use earlier factsL24–26

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

  1. L24
    apply mul_comm
  2. L25
    apply natural_mul_swap_right_tail
  3. L26
    apply natural_mul_swap_right_tail
07Calculate and transport equalitiesL27–32

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

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

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

  1. L33
    apply mul_comm
  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) * (q))))))
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–45

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
    refl
  4. L44
    congr
  5. L45
    trans ((m) * (((n) * (((n) * (m))))))
12Use earlier factsL46–46

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

  1. L46
    apply natural_mul_swap_right_tail
13Calculate and transport equalitiesL47–52

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

  1. L47
    congr
  2. L48
    refl
  3. L49
    trans ((m) * (((n) * (n))))
  4. L50
    trans ((n) * (((m) * (n))))
  5. L51
    congr
  6. L52
    refl
14Use earlier factsL53–54

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

  1. L53
    apply mul_comm
  2. 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) * (m))))))
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–66

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
    trans ((m) * (((p) * (p))))
  4. L64
    trans ((p) * (((m) * (p))))
  5. L65
    congr
  6. L66
    refl
18Use earlier factsL67–68

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

  1. L67
    apply mul_comm
  2. L68
    apply natural_mul_swap_right_tail
19Calculate and transport equalitiesL69–73

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

  1. L69
    congr
  2. L70
    refl
  3. L71
    refl
  4. L72
    congr
  5. L73
    trans ((m) * (((p) * (((n) * (q))))))
20Use earlier factsL74–74

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

  1. 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) * (q))))
22Use earlier factsL78–78

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

  1. L78
    apply natural_mul_swap_right_tail
23Calculate and transport equalitiesL79–88

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
    trans ((m) * (((n) * (((q) * (p))))))
  6. L84
    trans ((n) * (((m) * (((q) * (p))))))
  7. L85
    congr
  8. L86
    refl
  9. L87
    trans ((q) * (((m) * (p))))
  10. L88
    congr
24Calculate and transport equalitiesL89–89

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

  1. L89
    refl
25Use earlier factsL90–92

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

  1. L90
    apply mul_comm
  2. L91
    apply natural_mul_swap_right_tail
  3. L92
    apply natural_mul_swap_right_tail
26Calculate and transport equalitiesL93–97

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

  1. L93
    congr
  2. L94
    refl
  3. L95
    congr
  4. L96
    refl
  5. L97
    trans ((p) * (q))
27Use earlier factsL98–98

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

  1. L98
    apply mul_comm
28Calculate and transport equalitiesL99–104

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
    refl
  4. L102
    congr
  5. L103
    refl
  6. L104
    trans ((n) * (((q) * (q))))
29Use earlier factsL105–105

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

  1. L105
    apply natural_mul_swap_right_tail
30Calculate 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 ((((p) * (((p) * (((q) * (q))))))) + ((((m) * (((m) * (((p) * (p))))))) + ((((n) * (((n) * (((q) * (q))))))) + ((((m) * (((m) * (((n) * (n))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((m) * (((n) * (((p) * (q))))))))))))))
  5. L110
    congr
  6. L111
    refl
  7. L112
    trans ((((m) * (((m) * (((p) * (p))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((m) * (((n) * (n))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((n) * (((n) * (((q) * (q)))))))))))))
  8. L113
    trans ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((m) * (((p) * (p))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((m) * (((n) * (n))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((n) * (((n) * (((q) * (q)))))))))))))
  9. L114
    congr
  10. L115
    refl
31Calculate 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) * (((n) * (((p) * (q))))))) + ((((m) * (((m) * (((p) * (p))))))) + ((((m) * (((m) * (((n) * (n))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((n) * (((n) * (((q) * (q))))))))))))
  2. L117
    congr
  3. L118
    refl
32Use 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
33Calculate and transport equalitiesL122–131

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 ((((n) * (((n) * (((q) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((m) * (((n) * (n))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((m) * (((n) * (((p) * (q))))))))))))
  4. L125
    trans ((((m) * (((n) * (((p) * (q))))))) + ((((n) * (((n) * (((q) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((m) * (((n) * (n))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((m) * (((n) * (((p) * (q))))))))))))
  5. L126
    congr
  6. L127
    refl
  7. L128
    trans ((((m) * (((n) * (((p) * (q))))))) + ((((n) * (((n) * (((q) * (q))))))) + ((((m) * (((m) * (((n) * (n))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((m) * (((n) * (((p) * (q)))))))))))
  8. L129
    congr
  9. L130
    refl
  10. L131
    trans ((((m) * (((m) * (((n) * (n))))))) + ((((n) * (((n) * (((q) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((m) * (((n) * (((p) * (q))))))))))
34Calculate and transport equalitiesL132–136

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

  1. L132
    congr
  2. L133
    refl
  3. L134
    trans ((((m) * (((n) * (((p) * (q))))))) + ((((n) * (((n) * (((q) * (q))))))) + (((m) * (((n) * (((p) * (q)))))))))
  4. L135
    congr
  5. L136
    refl
35Use earlier factsL137–141

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

  1. L137
    apply add_comm
  2. L138
    apply four_square_add_swap_right_tail
  3. L139
    apply four_square_add_swap_right_tail
  4. L140
    apply four_square_add_swap_right_tail
  5. L141
    apply four_square_add_swap_right_tail
36Calculate and transport equalitiesL142–147

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

  1. L142
    congr
  2. L143
    refl
  3. L144
    trans ((((m) * (((m) * (((n) * (n))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((m) * (((n) * (((p) * (q)))))))))))
  4. L145
    trans ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((m) * (((n) * (n))))))) + ((((m) * (((n) * (((p) * (q))))))) + ((((m) * (((n) * (((p) * (q))))))) + (((m) * (((n) * (((p) * (q)))))))))))
  5. L146
    congr
  6. L147
    refl
37Use earlier factsL148–149

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
38Calculate and transport equalitiesL150–159

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

  1. L150
    congr
  2. L151
    refl
  3. L152
    refl
  4. L153
    trans ((((p) * (((p) * (((q) * (q))))))) + ((((p) * (((p) * (((m) * (m))))))) + ((((n) * (((n) * (((q) * (q))))))) + ((((n) * (((n) * (((m) * (m))))))) + ((((p) * (((n) * (((q) * (m))))))) + ((((p) * (((n) * (((m) * (q))))))) + ((((n) * (((p) * (((q) * (m))))))) + (((n) * (((p) * (((m) * (q))))))))))))))
  5. L154
    symm
  6. L155
    congr
  7. L156
    refl
  8. L157
    congr
  9. L158
    trans ((m) * (((p) * (((p) * (m))))))
  10. L159
    trans ((p) * (((m) * (((p) * (m))))))
39Calculate and transport equalitiesL160–161

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

  1. L160
    congr
  2. L161
    refl
40Use earlier factsL162–163

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

  1. L162
    apply natural_mul_swap_right_tail
  2. L163
    apply natural_mul_swap_right_tail
41Calculate and transport equalitiesL164–169

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 ((m) * (((p) * (p))))
  4. L167
    trans ((p) * (((m) * (p))))
  5. L168
    congr
  6. L169
    refl
42Use earlier factsL170–171

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

  1. L170
    apply mul_comm
  2. L171
    apply natural_mul_swap_right_tail
43Calculate and transport equalitiesL172–181

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

  1. L172
    congr
  2. L173
    refl
  3. L174
    refl
  4. L175
    congr
  5. L176
    refl
  6. L177
    congr
  7. L178
    trans ((m) * (((n) * (((n) * (m))))))
  8. L179
    trans ((n) * (((m) * (((n) * (m))))))
  9. L180
    congr
  10. L181
    refl
44Use earlier factsL182–183

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

  1. L182
    apply natural_mul_swap_right_tail
  2. L183
    apply natural_mul_swap_right_tail
45Calculate and transport equalitiesL184–189

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 ((m) * (((n) * (n))))
  4. L187
    trans ((n) * (((m) * (n))))
  5. L188
    congr
  6. L189
    refl
46Use earlier factsL190–191

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

  1. L190
    apply mul_comm
  2. L191
    apply natural_mul_swap_right_tail
47Calculate and transport equalitiesL192–201

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

  1. L192
    congr
  2. L193
    refl
  3. L194
    refl
  4. L195
    congr
  5. L196
    trans ((m) * (((p) * (((n) * (q))))))
  6. L197
    trans ((p) * (((m) * (((n) * (q))))))
  7. L198
    congr
  8. L199
    refl
  9. L200
    trans ((n) * (((m) * (q))))
  10. L201
    congr
48Calculate and transport equalitiesL202–202

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

  1. L202
    refl
49Use earlier factsL203–205

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

  1. L203
    apply mul_comm
  2. L204
    apply natural_mul_swap_right_tail
  3. L205
    apply natural_mul_swap_right_tail
50Calculate and transport equalitiesL206–208

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

  1. L206
    congr
  2. L207
    refl
  3. L208
    trans ((n) * (((p) * (q))))
51Use earlier factsL209–209

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

  1. L209
    apply natural_mul_swap_right_tail
52Calculate 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) * (q))))))
  6. L215
    trans ((p) * (((m) * (((n) * (q))))))
  7. L216
    congr
  8. L217
    refl
53Use 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
54Calculate and transport equalitiesL220–222

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 ((n) * (((p) * (q))))
55Use earlier factsL223–223

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

  1. L223
    apply natural_mul_swap_right_tail
56Calculate and transport equalitiesL224–233

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
    refl
  4. L227
    congr
  5. L228
    trans ((m) * (((n) * (((p) * (q))))))
  6. L229
    trans ((n) * (((m) * (((p) * (q))))))
  7. L230
    congr
  8. L231
    refl
  9. L232
    trans ((p) * (((m) * (q))))
  10. L233
    congr
57Calculate and transport equalitiesL234–234

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

  1. L234
    refl
58Use earlier factsL235–237

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

  1. L235
    apply mul_comm
  2. L236
    apply natural_mul_swap_right_tail
  3. L237
    apply natural_mul_swap_right_tail
59Calculate and transport equalitiesL238–244

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

  1. L238
    congr
  2. L239
    refl
  3. L240
    refl
  4. L241
    trans ((m) * (((n) * (((p) * (q))))))
  5. L242
    trans ((n) * (((m) * (((p) * (q))))))
  6. L243
    congr
  7. L244
    refl
60Use earlier factsL245–246

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

  1. L245
    apply natural_mul_swap_right_tail
  2. L246
    apply natural_mul_swap_right_tail
61Calculate and transport equalitiesL247–251

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

  1. L247
    congr
  2. L248
    refl
  3. L249
    refl
  4. L250
    symm
  5. L251
    simp [add_mul, mul_add, mul_assoc, add_assoc]

Library-wide reading audit

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