BT001P

division_remainder_exists

Stable · empty-context checked

Every positive divisor admits a quotient and a strictly bounded remainder.

Exact expanded PA statement

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

Structural proof guide

Every positive divisor admits a quotient and a strictly bounded remainder.

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

Proof neighborhood

Direct dependencies

BT000Q zero_or_succ BT001O division_remainder_succ

Direct dependents

BT002U gcd_exists_up_to BT0034 gcd_balanced_bezout_exists_up_to BT003B multiple_decidable_nonzero BT003X mod_eq_to_remainder_decomposition BT0041 beta_at_exists BT00R1 ceil_div_six_total BT00S0 prime_power_quotient_prefix_exists BT00X1 six_block_window_decomposition_above_thirty_two BT0115 bertrand_eventually_closed_upper

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. 0004specialize zero_or_succ m
  5. 0005cases zero_or_succ
  6. 0006exfalso
  7. 0007apply hm
  8. 0008exact zero_or_succ_left
  9. 0009cases zero_or_succ_right
  10. 0010specialize division_remainder_succ x
  11. 0011specialize division_remainder_succ n
  12. 0012rewrite zero_or_succ_right_witness
  13. 0013rewrite zero_or_succ_right_witness
  14. 0014exact division_remainder_succ