BT001W

multiple_has_zero_remainder

Stable · empty-context checked

Every multiple of a nonzero divisor has a bounded zero-remainder decomposition.

Exact expanded PA statement

forall m n. ~(m = 0) -> (exists q. n = m * q) -> exists q r. (n = m * q + r /\ r = 0) /\ S r <= m

Structural proof guide

Every multiple of a nonzero divisor has a bounded zero-remainder decomposition.

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

Proof neighborhood

Direct dependencies

BT000Q zero_or_succ

Direct dependents

BT003B multiple_decidable_nonzero BT00SH division_successor_quotient_by_bit

Formal native tactic body

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

  1. 0001intro m
  2. 0002intro n
  3. 0003intro hm
  4. 0004intro hd
  5. 0005cases hd
  6. 0006specialize zero_or_succ m
  7. 0007cases zero_or_succ
  8. 0008exfalso
  9. 0009apply hm
  10. 0010exact zero_or_succ_left
  11. 0011cases zero_or_succ_right
  12. 0012exists x
  13. 0013exists 0
  14. 0014split
  15. 0015split
  16. 0016rewrite hd_witness
  17. 0017simp
  18. 0018refl
  19. 0019exists x1
  20. 0020rewrite zero_or_succ_right_witness
  21. 0021simp