PA005P

square_residue_lift

Stable checked-use theorem · independently closed

Lift one quotient-and-remainder equation through squaring.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Lift one quotient-and-remainder equation through squaring.

Use the direct prerequisites square_decomp, add_residue as previously established PA formulas.

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA005N square_decomp PA005O add_residue

Proof neighborhood

Direct dependencies

PA005N square_decomp PA005O add_residue

Direct dependents

PA005Q square_residue_witness

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 c
  6. 0006intro s
  7. 0007intro hz
  8. 0008intro hrc
  9. 0009trans a * (q * z + r * q) + r * r
  10. 0010apply square_decomp
  11. 0011exact hz
  12. 0012apply add_residue
  13. 0013exact hrc