EI000E

eisenstein_weighted_embedding_compensation

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

The elementary compensation proves 4N=(2a-b)²+3b² without integer subtraction or an inequality assumption.

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 sa sb P Q sh N. (sa + sb) + Q = P + N -> (sh + (2 * P + 2 * P) = ((2 * 2) * sa + sb) + (2 * Q + 2 * Q)) -> sh + 3 * sb = 4 * N

Constructive proof overview

Generated structural guide

The elementary compensation proves 4N=(2a-b)²+3b² without integer subtraction or an inequality assumption.

The unchanged tactic script uses 12 declared prerequisites and contains 324 exact native proof lines.

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

Proof neighborhood

Direct dependencies

add_right_cancel Stable theorem; checked-use authorized 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 four_square_add_swap_right_tail Alpha theorem; checked-use authorized mul_succ_left Stable theorem; checked-use authorized mul_zero_left Stable theorem; checked-use authorized zero_add Stable theorem; checked-use authorized one_mul Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized

Direct dependents

EI000F eisenstein_norm_weighted_square_identity

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

324 script commands · 48 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.

01Fix variables and assumptionsL1–8

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

  1. L1
    intro sa
  2. L2
    intro sb
  3. L3
    intro P
  4. L4
    intro Q
  5. L5
    intro sh
  6. L6
    intro N
  7. L7
    intro hnorm
  8. L8
    intro hdifference
02Use earlier factsL9–12

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

  1. L9
    specialize add_right_cancel (sh + 3 * sb)
  2. L10
    specialize add_right_cancel (4 * N)
  3. L11
    specialize add_right_cancel (4 * P)
  4. L12
    apply add_right_cancel
03Calculate and transport equalitiesL13–22

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

  1. L13
    trans (sh + (2 * P + 2 * P)) + 3 * sb
  2. L14
    trans ((sh) + ((sb) + ((sb) + ((sb) + ((P) + ((P) + ((P) + (P))))))))
  3. L15
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  4. L16
    trans ((sh) + ((sb) + ((sb) + ((sb) + ((P) + ((P) + ((P) + (P))))))))
  5. L17
    congr
  6. L18
    refl
  7. L19
    congr
  8. L20
    refl
  9. L21
    congr
  10. L22
    refl
04Calculate and transport equalitiesL23–32

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

  1. L23
    congr
  2. L24
    refl
  3. L25
    congr
  4. L26
    refl
  5. L27
    congr
  6. L28
    refl
  7. L29
    congr
  8. L30
    refl
  9. L31
    refl
  10. L32
    trans ((sh) + ((P) + ((P) + ((P) + ((P) + ((sb) + ((sb) + (sb))))))))
05Calculate and transport equalitiesL33–41

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

  1. L33
    congr
  2. L34
    refl
  3. L35
    trans ((P) + ((sb) + ((sb) + ((sb) + ((P) + ((P) + (P)))))))
  4. L36
    trans ((sb) + ((P) + ((sb) + ((sb) + ((P) + ((P) + (P)))))))
  5. L37
    congr
  6. L38
    refl
  7. L39
    trans ((sb) + ((P) + ((sb) + ((P) + ((P) + (P))))))
  8. L40
    congr
  9. L41
    refl
06Use earlier factsL42–44

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

  1. L42
    apply four_square_add_swap_right_tail
  2. L43
    apply four_square_add_swap_right_tail
  3. L44
    apply four_square_add_swap_right_tail
07Calculate and transport equalitiesL45–53

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

  1. L45
    congr
  2. L46
    refl
  3. L47
    trans ((P) + ((sb) + ((sb) + ((sb) + ((P) + (P))))))
  4. L48
    trans ((sb) + ((P) + ((sb) + ((sb) + ((P) + (P))))))
  5. L49
    congr
  6. L50
    refl
  7. L51
    trans ((sb) + ((P) + ((sb) + ((P) + (P)))))
  8. L52
    congr
  9. L53
    refl
08Use earlier factsL54–56

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

  1. L54
    apply four_square_add_swap_right_tail
  2. L55
    apply four_square_add_swap_right_tail
  3. L56
    apply four_square_add_swap_right_tail
09Calculate and transport equalitiesL57–65

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

  1. L57
    congr
  2. L58
    refl
  3. L59
    trans ((P) + ((sb) + ((sb) + ((sb) + (P)))))
  4. L60
    trans ((sb) + ((P) + ((sb) + ((sb) + (P)))))
  5. L61
    congr
  6. L62
    refl
  7. L63
    trans ((sb) + ((P) + ((sb) + (P))))
  8. L64
    congr
  9. L65
    refl
10Use earlier factsL66–68

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

  1. L66
    apply four_square_add_swap_right_tail
  2. L67
    apply four_square_add_swap_right_tail
  3. L68
    apply four_square_add_swap_right_tail
11Calculate and transport equalitiesL69–77

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
    trans ((P) + ((sb) + ((sb) + (sb))))
  4. L72
    trans ((sb) + ((P) + ((sb) + (sb))))
  5. L73
    congr
  6. L74
    refl
  7. L75
    trans ((sb) + ((P) + (sb)))
  8. L76
    congr
  9. L77
    refl
12Use earlier factsL78–80

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

  1. L78
    apply add_comm
  2. L79
    apply four_square_add_swap_right_tail
  3. L80
    apply four_square_add_swap_right_tail
13Calculate and transport equalitiesL81–90

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

  1. L81
    congr
  2. L82
    refl
  3. L83
    refl
  4. L84
    trans ((sh) + ((P) + ((P) + ((P) + ((P) + ((sb) + ((sb) + (sb))))))))
  5. L85
    symm
  6. L86
    congr
  7. L87
    refl
  8. L88
    congr
  9. L89
    refl
  10. L90
    congr
14Calculate and transport equalitiesL91–100

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

  1. L91
    refl
  2. L92
    congr
  3. L93
    refl
  4. L94
    congr
  5. L95
    refl
  6. L96
    congr
  7. L97
    refl
  8. L98
    congr
  9. L99
    refl
  10. L100
    refl
15Calculate and transport equalitiesL101–110

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

  1. L101
    symm
  2. L102
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  3. L103
    rewrite hdifference
  4. L104
    trans 4 * ((sa + sb) + Q)
  5. L105
    trans ((sa) + ((sa) + ((sa) + ((sa) + ((sb) + ((Q) + ((Q) + ((Q) + ((Q) + ((sb) + ((sb) + (sb))))))))))))
  6. L106
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  7. L107
    trans ((sa) + ((sa) + ((sa) + ((sa) + ((sb) + ((Q) + ((Q) + ((Q) + ((Q) + ((sb) + ((sb) + (sb))))))))))))
  8. L108
    congr
  9. L109
    refl
  10. L110
    congr
16Calculate and transport equalitiesL111–120

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

  1. L111
    refl
  2. L112
    congr
  3. L113
    refl
  4. L114
    congr
  5. L115
    refl
  6. L116
    congr
  7. L117
    refl
  8. L118
    congr
  9. L119
    refl
  10. L120
    congr
17Calculate and transport equalitiesL121–130

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

  1. L121
    refl
  2. L122
    congr
  3. L123
    refl
  4. L124
    congr
  5. L125
    refl
  6. L126
    congr
  7. L127
    refl
  8. L128
    congr
  9. L129
    refl
  10. L130
    refl
18Calculate and transport equalitiesL131–140

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

  1. L131
    trans ((sa) + ((sa) + ((sa) + ((sa) + ((sb) + ((sb) + ((sb) + ((sb) + ((Q) + ((Q) + ((Q) + (Q))))))))))))
  2. L132
    congr
  3. L133
    refl
  4. L134
    congr
  5. L135
    refl
  6. L136
    congr
  7. L137
    refl
  8. L138
    congr
  9. L139
    refl
  10. L140
    congr
19Calculate and transport equalitiesL141–150

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

  1. L141
    refl
  2. L142
    trans ((sb) + ((Q) + ((Q) + ((Q) + ((Q) + ((sb) + (sb)))))))
  3. L143
    trans ((Q) + ((sb) + ((Q) + ((Q) + ((Q) + ((sb) + (sb)))))))
  4. L144
    congr
  5. L145
    refl
  6. L146
    trans ((Q) + ((sb) + ((Q) + ((Q) + ((sb) + (sb))))))
  7. L147
    congr
  8. L148
    refl
  9. L149
    trans ((Q) + ((sb) + ((Q) + ((sb) + (sb)))))
  10. L150
    congr
20Calculate and transport equalitiesL151–151

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

  1. L151
    refl
21Use earlier factsL152–155

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

  1. L152
    apply four_square_add_swap_right_tail
  2. L153
    apply four_square_add_swap_right_tail
  3. L154
    apply four_square_add_swap_right_tail
  4. L155
    apply four_square_add_swap_right_tail
22Calculate and transport equalitiesL156–165

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

  1. L156
    congr
  2. L157
    refl
  3. L158
    trans ((sb) + ((Q) + ((Q) + ((Q) + ((Q) + (sb))))))
  4. L159
    trans ((Q) + ((sb) + ((Q) + ((Q) + ((Q) + (sb))))))
  5. L160
    congr
  6. L161
    refl
  7. L162
    trans ((Q) + ((sb) + ((Q) + ((Q) + (sb)))))
  8. L163
    congr
  9. L164
    refl
  10. L165
    trans ((Q) + ((sb) + ((Q) + (sb))))
23Calculate and transport equalitiesL166–167

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

  1. L166
    congr
  2. L167
    refl
24Use earlier factsL168–171

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

  1. L168
    apply four_square_add_swap_right_tail
  2. L169
    apply four_square_add_swap_right_tail
  3. L170
    apply four_square_add_swap_right_tail
  4. L171
    apply four_square_add_swap_right_tail
25Calculate 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
    trans ((sb) + ((Q) + ((Q) + ((Q) + (Q)))))
  4. L175
    trans ((Q) + ((sb) + ((Q) + ((Q) + (Q)))))
  5. L176
    congr
  6. L177
    refl
  7. L178
    trans ((Q) + ((sb) + ((Q) + (Q))))
  8. L179
    congr
  9. L180
    refl
  10. L181
    trans ((Q) + ((sb) + (Q)))
26Calculate and transport equalitiesL182–183

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

  1. L182
    congr
  2. L183
    refl
27Use earlier factsL184–187

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

  1. L184
    apply add_comm
  2. L185
    apply four_square_add_swap_right_tail
  3. L186
    apply four_square_add_swap_right_tail
  4. L187
    apply four_square_add_swap_right_tail
28Calculate and transport equalitiesL188–197

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

  1. L188
    congr
  2. L189
    refl
  3. L190
    refl
  4. L191
    trans ((sa) + ((sa) + ((sa) + ((sa) + ((sb) + ((sb) + ((sb) + ((sb) + ((Q) + ((Q) + ((Q) + (Q))))))))))))
  5. L192
    symm
  6. L193
    congr
  7. L194
    refl
  8. L195
    congr
  9. L196
    refl
  10. L197
    congr
29Calculate and transport equalitiesL198–207

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

  1. L198
    refl
  2. L199
    congr
  3. L200
    refl
  4. L201
    congr
  5. L202
    refl
  6. L203
    congr
  7. L204
    refl
  8. L205
    congr
  9. L206
    refl
  10. L207
    congr
30Calculate and transport equalitiesL208–217

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

  1. L208
    refl
  2. L209
    congr
  3. L210
    refl
  4. L211
    congr
  5. L212
    refl
  6. L213
    congr
  7. L214
    refl
  8. L215
    refl
  9. L216
    symm
  10. L217
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
31Calculate and transport equalitiesL218–220

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

  1. L218
    trans 4 * (P + N)
  2. L219
    congr
  3. L220
    refl
32Use earlier factsL221–221

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

  1. L221
    exact hnorm
33Calculate and transport equalitiesL222–231

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

  1. L222
    trans ((P) + ((P) + ((P) + ((P) + ((N) + ((N) + ((N) + (N))))))))
  2. L223
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  3. L224
    trans ((P) + ((P) + ((P) + ((P) + ((N) + ((N) + ((N) + (N))))))))
  4. L225
    congr
  5. L226
    refl
  6. L227
    congr
  7. L228
    refl
  8. L229
    congr
  9. L230
    refl
  10. L231
    congr
34Calculate and transport equalitiesL232–241

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

  1. L232
    refl
  2. L233
    congr
  3. L234
    refl
  4. L235
    congr
  5. L236
    refl
  6. L237
    congr
  7. L238
    refl
  8. L239
    refl
  9. L240
    trans ((N) + ((N) + ((N) + ((N) + ((P) + ((P) + ((P) + (P))))))))
  10. L241
    trans ((N) + ((P) + ((P) + ((P) + ((P) + ((N) + ((N) + (N))))))))
35Calculate and transport equalitiesL242–250

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

  1. L242
    trans ((P) + ((N) + ((P) + ((P) + ((P) + ((N) + ((N) + (N))))))))
  2. L243
    congr
  3. L244
    refl
  4. L245
    trans ((P) + ((N) + ((P) + ((P) + ((N) + ((N) + (N)))))))
  5. L246
    congr
  6. L247
    refl
  7. L248
    trans ((P) + ((N) + ((P) + ((N) + ((N) + (N))))))
  8. L249
    congr
  9. L250
    refl
36Use earlier factsL251–254

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

  1. L251
    apply four_square_add_swap_right_tail
  2. L252
    apply four_square_add_swap_right_tail
  3. L253
    apply four_square_add_swap_right_tail
  4. L254
    apply four_square_add_swap_right_tail
37Calculate and transport equalitiesL255–264

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

  1. L255
    congr
  2. L256
    refl
  3. L257
    trans ((N) + ((P) + ((P) + ((P) + ((P) + ((N) + (N)))))))
  4. L258
    trans ((P) + ((N) + ((P) + ((P) + ((P) + ((N) + (N)))))))
  5. L259
    congr
  6. L260
    refl
  7. L261
    trans ((P) + ((N) + ((P) + ((P) + ((N) + (N))))))
  8. L262
    congr
  9. L263
    refl
  10. L264
    trans ((P) + ((N) + ((P) + ((N) + (N)))))
38Calculate and transport equalitiesL265–266

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

  1. L265
    congr
  2. L266
    refl
39Use earlier factsL267–270

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

  1. L267
    apply four_square_add_swap_right_tail
  2. L268
    apply four_square_add_swap_right_tail
  3. L269
    apply four_square_add_swap_right_tail
  4. L270
    apply four_square_add_swap_right_tail
40Calculate and transport equalitiesL271–280

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

  1. L271
    congr
  2. L272
    refl
  3. L273
    trans ((N) + ((P) + ((P) + ((P) + ((P) + (N))))))
  4. L274
    trans ((P) + ((N) + ((P) + ((P) + ((P) + (N))))))
  5. L275
    congr
  6. L276
    refl
  7. L277
    trans ((P) + ((N) + ((P) + ((P) + (N)))))
  8. L278
    congr
  9. L279
    refl
  10. L280
    trans ((P) + ((N) + ((P) + (N))))
41Calculate and transport equalitiesL281–282

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

  1. L281
    congr
  2. L282
    refl
42Use earlier factsL283–286

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

  1. L283
    apply four_square_add_swap_right_tail
  2. L284
    apply four_square_add_swap_right_tail
  3. L285
    apply four_square_add_swap_right_tail
  4. L286
    apply four_square_add_swap_right_tail
43Calculate and transport equalitiesL287–296

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

  1. L287
    congr
  2. L288
    refl
  3. L289
    trans ((N) + ((P) + ((P) + ((P) + (P)))))
  4. L290
    trans ((P) + ((N) + ((P) + ((P) + (P)))))
  5. L291
    congr
  6. L292
    refl
  7. L293
    trans ((P) + ((N) + ((P) + (P))))
  8. L294
    congr
  9. L295
    refl
  10. L296
    trans ((P) + ((N) + (P)))
44Calculate and transport equalitiesL297–298

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

  1. L297
    congr
  2. L298
    refl
45Use earlier factsL299–302

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

  1. L299
    apply add_comm
  2. L300
    apply four_square_add_swap_right_tail
  3. L301
    apply four_square_add_swap_right_tail
  4. L302
    apply four_square_add_swap_right_tail
46Calculate and transport equalitiesL303–312

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

  1. L303
    congr
  2. L304
    refl
  3. L305
    refl
  4. L306
    trans ((N) + ((N) + ((N) + ((N) + ((P) + ((P) + ((P) + (P))))))))
  5. L307
    symm
  6. L308
    congr
  7. L309
    refl
  8. L310
    congr
  9. L311
    refl
  10. L312
    congr
47Calculate and transport equalitiesL313–322

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

  1. L313
    refl
  2. L314
    congr
  3. L315
    refl
  4. L316
    congr
  5. L317
    refl
  6. L318
    congr
  7. L319
    refl
  8. L320
    congr
  9. L321
    refl
  10. L322
    refl
48Calculate and transport equalitiesL323–324

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

  1. L323
    symm
  2. L324
    simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]

Library-wide reading audit

Original exact command ledger · 324 lines
  1. 0001intro sa
  2. 0002intro sb
  3. 0003intro P
  4. 0004intro Q
  5. 0005intro sh
  6. 0006intro N
  7. 0007intro hnorm
  8. 0008intro hdifference
  9. 0009specialize add_right_cancel (sh + 3 * sb)
  10. 0010specialize add_right_cancel (4 * N)
  11. 0011specialize add_right_cancel (4 * P)
  12. 0012apply add_right_cancel
  13. 0013trans (sh + (2 * P + 2 * P)) + 3 * sb
  14. 0014trans ((sh) + ((sb) + ((sb) + ((sb) + ((P) + ((P) + ((P) + (P))))))))
  15. 0015simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  16. 0016trans ((sh) + ((sb) + ((sb) + ((sb) + ((P) + ((P) + ((P) + (P))))))))
  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. 0031refl
  32. 0032trans ((sh) + ((P) + ((P) + ((P) + ((P) + ((sb) + ((sb) + (sb))))))))
  33. 0033congr
  34. 0034refl
  35. 0035trans ((P) + ((sb) + ((sb) + ((sb) + ((P) + ((P) + (P)))))))
  36. 0036trans ((sb) + ((P) + ((sb) + ((sb) + ((P) + ((P) + (P)))))))
  37. 0037congr
  38. 0038refl
  39. 0039trans ((sb) + ((P) + ((sb) + ((P) + ((P) + (P))))))
  40. 0040congr
  41. 0041refl
  42. 0042apply four_square_add_swap_right_tail
  43. 0043apply four_square_add_swap_right_tail
  44. 0044apply four_square_add_swap_right_tail
  45. 0045congr
  46. 0046refl
  47. 0047trans ((P) + ((sb) + ((sb) + ((sb) + ((P) + (P))))))
  48. 0048trans ((sb) + ((P) + ((sb) + ((sb) + ((P) + (P))))))
  49. 0049congr
  50. 0050refl
  51. 0051trans ((sb) + ((P) + ((sb) + ((P) + (P)))))
  52. 0052congr
  53. 0053refl
  54. 0054apply four_square_add_swap_right_tail
  55. 0055apply four_square_add_swap_right_tail
  56. 0056apply four_square_add_swap_right_tail
  57. 0057congr
  58. 0058refl
  59. 0059trans ((P) + ((sb) + ((sb) + ((sb) + (P)))))
  60. 0060trans ((sb) + ((P) + ((sb) + ((sb) + (P)))))
  61. 0061congr
  62. 0062refl
  63. 0063trans ((sb) + ((P) + ((sb) + (P))))
  64. 0064congr
  65. 0065refl
  66. 0066apply four_square_add_swap_right_tail
  67. 0067apply four_square_add_swap_right_tail
  68. 0068apply four_square_add_swap_right_tail
  69. 0069congr
  70. 0070refl
  71. 0071trans ((P) + ((sb) + ((sb) + (sb))))
  72. 0072trans ((sb) + ((P) + ((sb) + (sb))))
  73. 0073congr
  74. 0074refl
  75. 0075trans ((sb) + ((P) + (sb)))
  76. 0076congr
  77. 0077refl
  78. 0078apply add_comm
  79. 0079apply four_square_add_swap_right_tail
  80. 0080apply four_square_add_swap_right_tail
  81. 0081congr
  82. 0082refl
  83. 0083refl
  84. 0084trans ((sh) + ((P) + ((P) + ((P) + ((P) + ((sb) + ((sb) + (sb))))))))
  85. 0085symm
  86. 0086congr
  87. 0087refl
  88. 0088congr
  89. 0089refl
  90. 0090congr
  91. 0091refl
  92. 0092congr
  93. 0093refl
  94. 0094congr
  95. 0095refl
  96. 0096congr
  97. 0097refl
  98. 0098congr
  99. 0099refl
  100. 0100refl
  101. 0101symm
  102. 0102simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  103. 0103rewrite hdifference
  104. 0104trans 4 * ((sa + sb) + Q)
  105. 0105trans ((sa) + ((sa) + ((sa) + ((sa) + ((sb) + ((Q) + ((Q) + ((Q) + ((Q) + ((sb) + ((sb) + (sb))))))))))))
  106. 0106simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  107. 0107trans ((sa) + ((sa) + ((sa) + ((sa) + ((sb) + ((Q) + ((Q) + ((Q) + ((Q) + ((sb) + ((sb) + (sb))))))))))))
  108. 0108congr
  109. 0109refl
  110. 0110congr
  111. 0111refl
  112. 0112congr
  113. 0113refl
  114. 0114congr
  115. 0115refl
  116. 0116congr
  117. 0117refl
  118. 0118congr
  119. 0119refl
  120. 0120congr
  121. 0121refl
  122. 0122congr
  123. 0123refl
  124. 0124congr
  125. 0125refl
  126. 0126congr
  127. 0127refl
  128. 0128congr
  129. 0129refl
  130. 0130refl
  131. 0131trans ((sa) + ((sa) + ((sa) + ((sa) + ((sb) + ((sb) + ((sb) + ((sb) + ((Q) + ((Q) + ((Q) + (Q))))))))))))
  132. 0132congr
  133. 0133refl
  134. 0134congr
  135. 0135refl
  136. 0136congr
  137. 0137refl
  138. 0138congr
  139. 0139refl
  140. 0140congr
  141. 0141refl
  142. 0142trans ((sb) + ((Q) + ((Q) + ((Q) + ((Q) + ((sb) + (sb)))))))
  143. 0143trans ((Q) + ((sb) + ((Q) + ((Q) + ((Q) + ((sb) + (sb)))))))
  144. 0144congr
  145. 0145refl
  146. 0146trans ((Q) + ((sb) + ((Q) + ((Q) + ((sb) + (sb))))))
  147. 0147congr
  148. 0148refl
  149. 0149trans ((Q) + ((sb) + ((Q) + ((sb) + (sb)))))
  150. 0150congr
  151. 0151refl
  152. 0152apply four_square_add_swap_right_tail
  153. 0153apply four_square_add_swap_right_tail
  154. 0154apply four_square_add_swap_right_tail
  155. 0155apply four_square_add_swap_right_tail
  156. 0156congr
  157. 0157refl
  158. 0158trans ((sb) + ((Q) + ((Q) + ((Q) + ((Q) + (sb))))))
  159. 0159trans ((Q) + ((sb) + ((Q) + ((Q) + ((Q) + (sb))))))
  160. 0160congr
  161. 0161refl
  162. 0162trans ((Q) + ((sb) + ((Q) + ((Q) + (sb)))))
  163. 0163congr
  164. 0164refl
  165. 0165trans ((Q) + ((sb) + ((Q) + (sb))))
  166. 0166congr
  167. 0167refl
  168. 0168apply four_square_add_swap_right_tail
  169. 0169apply four_square_add_swap_right_tail
  170. 0170apply four_square_add_swap_right_tail
  171. 0171apply four_square_add_swap_right_tail
  172. 0172congr
  173. 0173refl
  174. 0174trans ((sb) + ((Q) + ((Q) + ((Q) + (Q)))))
  175. 0175trans ((Q) + ((sb) + ((Q) + ((Q) + (Q)))))
  176. 0176congr
  177. 0177refl
  178. 0178trans ((Q) + ((sb) + ((Q) + (Q))))
  179. 0179congr
  180. 0180refl
  181. 0181trans ((Q) + ((sb) + (Q)))
  182. 0182congr
  183. 0183refl
  184. 0184apply add_comm
  185. 0185apply four_square_add_swap_right_tail
  186. 0186apply four_square_add_swap_right_tail
  187. 0187apply four_square_add_swap_right_tail
  188. 0188congr
  189. 0189refl
  190. 0190refl
  191. 0191trans ((sa) + ((sa) + ((sa) + ((sa) + ((sb) + ((sb) + ((sb) + ((sb) + ((Q) + ((Q) + ((Q) + (Q))))))))))))
  192. 0192symm
  193. 0193congr
  194. 0194refl
  195. 0195congr
  196. 0196refl
  197. 0197congr
  198. 0198refl
  199. 0199congr
  200. 0200refl
  201. 0201congr
  202. 0202refl
  203. 0203congr
  204. 0204refl
  205. 0205congr
  206. 0206refl
  207. 0207congr
  208. 0208refl
  209. 0209congr
  210. 0210refl
  211. 0211congr
  212. 0212refl
  213. 0213congr
  214. 0214refl
  215. 0215refl
  216. 0216symm
  217. 0217simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  218. 0218trans 4 * (P + N)
  219. 0219congr
  220. 0220refl
  221. 0221exact hnorm
  222. 0222trans ((P) + ((P) + ((P) + ((P) + ((N) + ((N) + ((N) + (N))))))))
  223. 0223simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]
  224. 0224trans ((P) + ((P) + ((P) + ((P) + ((N) + ((N) + ((N) + (N))))))))
  225. 0225congr
  226. 0226refl
  227. 0227congr
  228. 0228refl
  229. 0229congr
  230. 0230refl
  231. 0231congr
  232. 0232refl
  233. 0233congr
  234. 0234refl
  235. 0235congr
  236. 0236refl
  237. 0237congr
  238. 0238refl
  239. 0239refl
  240. 0240trans ((N) + ((N) + ((N) + ((N) + ((P) + ((P) + ((P) + (P))))))))
  241. 0241trans ((N) + ((P) + ((P) + ((P) + ((P) + ((N) + ((N) + (N))))))))
  242. 0242trans ((P) + ((N) + ((P) + ((P) + ((P) + ((N) + ((N) + (N))))))))
  243. 0243congr
  244. 0244refl
  245. 0245trans ((P) + ((N) + ((P) + ((P) + ((N) + ((N) + (N)))))))
  246. 0246congr
  247. 0247refl
  248. 0248trans ((P) + ((N) + ((P) + ((N) + ((N) + (N))))))
  249. 0249congr
  250. 0250refl
  251. 0251apply four_square_add_swap_right_tail
  252. 0252apply four_square_add_swap_right_tail
  253. 0253apply four_square_add_swap_right_tail
  254. 0254apply four_square_add_swap_right_tail
  255. 0255congr
  256. 0256refl
  257. 0257trans ((N) + ((P) + ((P) + ((P) + ((P) + ((N) + (N)))))))
  258. 0258trans ((P) + ((N) + ((P) + ((P) + ((P) + ((N) + (N)))))))
  259. 0259congr
  260. 0260refl
  261. 0261trans ((P) + ((N) + ((P) + ((P) + ((N) + (N))))))
  262. 0262congr
  263. 0263refl
  264. 0264trans ((P) + ((N) + ((P) + ((N) + (N)))))
  265. 0265congr
  266. 0266refl
  267. 0267apply four_square_add_swap_right_tail
  268. 0268apply four_square_add_swap_right_tail
  269. 0269apply four_square_add_swap_right_tail
  270. 0270apply four_square_add_swap_right_tail
  271. 0271congr
  272. 0272refl
  273. 0273trans ((N) + ((P) + ((P) + ((P) + ((P) + (N))))))
  274. 0274trans ((P) + ((N) + ((P) + ((P) + ((P) + (N))))))
  275. 0275congr
  276. 0276refl
  277. 0277trans ((P) + ((N) + ((P) + ((P) + (N)))))
  278. 0278congr
  279. 0279refl
  280. 0280trans ((P) + ((N) + ((P) + (N))))
  281. 0281congr
  282. 0282refl
  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. 0287congr
  288. 0288refl
  289. 0289trans ((N) + ((P) + ((P) + ((P) + (P)))))
  290. 0290trans ((P) + ((N) + ((P) + ((P) + (P)))))
  291. 0291congr
  292. 0292refl
  293. 0293trans ((P) + ((N) + ((P) + (P))))
  294. 0294congr
  295. 0295refl
  296. 0296trans ((P) + ((N) + (P)))
  297. 0297congr
  298. 0298refl
  299. 0299apply add_comm
  300. 0300apply four_square_add_swap_right_tail
  301. 0301apply four_square_add_swap_right_tail
  302. 0302apply four_square_add_swap_right_tail
  303. 0303congr
  304. 0304refl
  305. 0305refl
  306. 0306trans ((N) + ((N) + ((N) + ((N) + ((P) + ((P) + ((P) + (P))))))))
  307. 0307symm
  308. 0308congr
  309. 0309refl
  310. 0310congr
  311. 0311refl
  312. 0312congr
  313. 0313refl
  314. 0314congr
  315. 0315refl
  316. 0316congr
  317. 0317refl
  318. 0318congr
  319. 0319refl
  320. 0320congr
  321. 0321refl
  322. 0322refl
  323. 0323symm
  324. 0324simp [add_mul, mul_add, mul_assoc, add_assoc, mul_succ_left, mul_zero_left, zero_add, one_mul, mul_one]