PA001G

divides_linear_step

Stable checked-use theorem · independently closed

A common divisor of a divisor and remainder divides their Euclidean linear step.

Exact expanded PA statement

forall c b q r. (exists u. b = c * u) -> (exists v. r = c * v) -> exists w. b * q + r = c * w

Structural proof guide

Generated structural guide

A common divisor of a divisor and remainder divides their Euclidean linear step.

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

The proof proceeds by case analysis (2), equality transport (2).

Referenced ingredients

PA000B mul_assoc PA000A mul_add

Proof neighborhood

Direct dependencies

PA000B mul_assoc PA000A mul_add

Direct dependents

PA001H is_gcd_euclid_forward

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 c
  2. 0002intro b
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hb
  6. 0006intro hr
  7. 0007cases hb
  8. 0008cases hr
  9. 0009exists x * q + x1
  10. 0010rewrite hb_witness
  11. 0011rewrite hr_witness
  12. 0012trans c * (x * q) + c * x1
  13. 0013congr
  14. 0014apply mul_assoc
  15. 0015refl
  16. 0016symm
  17. 0017apply mul_add