PA001D

division_remainder_exists

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites zero_or_succ, division_remainder_succ as previously established PA formulas.

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

Referenced ingredients

PA0008 zero_or_succ PA001C division_remainder_succ

Proof neighborhood

Direct dependencies

PA0008 zero_or_succ PA001C division_remainder_succ

Direct dependents

PA001K gcd_balanced_bezout_exists_up_to PA0029 beta_at_exists PA002V mod_eq_to_remainder_decomposition PA0035 gcd_exists_up_to PA005K mod_eq_decidable_nonzero PA005R quadratic_residue_bounded_equiv PA0063 prime_bounded_nonzero_mod_inverse PA0072 gauss_half_range_signed_choices PA0086 nondivisor_canonical_remainder_exists PA008B prime_mul_index_map_exists_up_to PA008Q prime_scaled_inverse_exists PA00BY beta_division_prefix_exists

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