PA005N

square_decomp

Stable checked-use theorem · independently closed

Expand a square while retaining an explicit quotient and remainder.

Exact expanded PA statement

forall a z q r. z = a * q + r -> z * z = a * (q * z + r * q) + r * r

Structural proof guide

Generated structural guide

Expand a square while retaining an explicit quotient and remainder.

Use the direct prerequisites add_assoc, mul_comm, mul_add, add_mul, mul_assoc as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA0009 add_assoc PA000H mul_comm PA000A mul_add PA0016 add_mul PA000B mul_assoc

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000H mul_comm PA000A mul_add PA0016 add_mul PA000B mul_assoc

Direct dependents

PA005P square_residue_lift

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro a
  2. 0002intro z
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hz
  6. 0006trans (a * q + r) * z
  7. 0007congr
  8. 0008exact hz
  9. 0009refl
  10. 0010trans (a * q) * z + r * z
  11. 0011apply add_mul
  12. 0012trans a * (q * z) + r * z
  13. 0013congr
  14. 0014apply mul_assoc
  15. 0015refl
  16. 0016trans a * (q * z) + r * (a * q + r)
  17. 0017congr
  18. 0018refl
  19. 0019congr
  20. 0020refl
  21. 0021exact hz
  22. 0022trans a * (q * z) + (r * (a * q) + r * r)
  23. 0023congr
  24. 0024refl
  25. 0025apply mul_add
  26. 0026trans a * (q * z) + (a * (r * q) + r * r)
  27. 0027congr
  28. 0028refl
  29. 0029congr
  30. 0030trans (r * a) * q
  31. 0031symm
  32. 0032apply mul_assoc
  33. 0033trans (a * r) * q
  34. 0034congr
  35. 0035apply mul_comm
  36. 0036refl
  37. 0037apply mul_assoc
  38. 0038refl
  39. 0039trans (a * (q * z) + a * (r * q)) + r * r
  40. 0040symm
  41. 0041apply add_assoc
  42. 0042congr
  43. 0043symm
  44. 0044apply mul_add
  45. 0045refl