BT002I

divides_linear_step

Stable · empty-context checked

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

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

Direct prerequisites: mul_assoc, mul_add. The authored body proceeds by case analysis (2), equality transport (2).

Proof neighborhood

Direct dependencies

BT0008 mul_assoc BT0007 mul_add

Direct dependents

BT002S is_gcd_euclid_forward

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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