PA005O

add_residue

Stable checked-use theorem · independently closed

Absorb a second quotient into an existing residue equation.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

Absorb a second quotient into an existing residue equation.

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

The proof proceeds by direct introduction and elimination.

Referenced ingredients

PA0009 add_assoc PA000A mul_add

Proof neighborhood

Direct dependencies

PA0009 add_assoc PA000A mul_add

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 u
  3. 0003intro c
  4. 0004intro r
  5. 0005intro s
  6. 0006intro hr
  7. 0007trans a * u + (a * c + s)
  8. 0008congr
  9. 0009refl
  10. 0010exact hr
  11. 0011trans (a * u + a * c) + s
  12. 0012symm
  13. 0013apply add_assoc
  14. 0014congr
  15. 0015symm
  16. 0016apply mul_add
  17. 0017refl