PA0014

divides_remainder

Stable checked-use theorem · independently closed

A common divisor of a dividend and divisor also divides the remainder.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

A common divisor of a dividend and divisor also divides the remainder.

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

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

Referenced ingredients

PA000B mul_assoc PA0013 factor_difference

Proof neighborhood

Direct dependencies

PA000B mul_assoc PA0013 factor_difference

Direct dependents

PA0015 beta_modulus_coprime_base PA0017 common_divisor_beta_moduli_divides_gap_times_c 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 a
  3. 0003intro b
  4. 0004intro q
  5. 0005intro r
  6. 0006intro ha
  7. 0007intro hb
  8. 0008intro h
  9. 0009cases ha
  10. 0010cases hb
  11. 0011specialize factor_difference c
  12. 0012specialize factor_difference x
  13. 0013specialize factor_difference (x1 * q)
  14. 0014specialize factor_difference r
  15. 0015apply factor_difference
  16. 0016trans a
  17. 0017symm
  18. 0018exact ha_witness
  19. 0019trans b * q + r
  20. 0020exact h
  21. 0021congr
  22. 0022rewrite hb_witness
  23. 0023apply mul_assoc
  24. 0024refl