BT002H

divides_remainder

Stable · empty-context checked

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

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

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

Proof neighborhood

Direct dependencies

BT0008 mul_assoc BT002G factor_difference

Direct dependents

BT002S is_gcd_euclid_forward BT004I beta_modulus_coprime_base BT004J common_divisor_beta_moduli_divides_gap_times_c BT011B nonzero_remainder_not_multiple

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 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