PA001C

division_remainder_succ

Stable checked-use theorem · independently closed

Every dividend has a quotient and bounded remainder for a successor divisor.

Exact expanded PA statement

forall d n. exists q r. n = S d * q + r /\ S r <= S d

Structural proof guide

Generated structural guide

Every dividend has a quotient and bounded remainder for a successor divisor.

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

The proof proceeds by structural induction (1), case analysis (6), intermediate claims (1), equality transport (7), certified simplification (6).

Referenced ingredients

PA0001 zero_add PA000E add_succ_left PA0008 zero_or_succ

Proof neighborhood

Direct dependencies

PA0001 zero_add PA000E add_succ_left PA0008 zero_or_succ

Direct dependents

PA001D division_remainder_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 d
  2. 0002induction n
  3. 0003exists 0
  4. 0004exists 0
  5. 0005split
  6. 0006simp
  7. 0007exists d
  8. 0008simp
  9. 0009cases IH
  10. 0010cases IH_witness
  11. 0011cases IH_witness_witness
  12. 0012cases IH_witness_witness_right
  13. 0013specialize zero_or_succ x2
  14. 0014cases zero_or_succ
  15. 0015rewrite zero_or_succ_left at IH_witness_witness_right_witness
  16. 0016specialize zero_add S x1
  17. 0017rewrite zero_add at IH_witness_witness_right_witness
  18. 0018have hrd : x1 = d
  19. 0019apply PA2
  20. 0020exact IH_witness_witness_right_witness
  21. 0021exists S x
  22. 0022exists 0
  23. 0023split
  24. 0024rewrite IH_witness_witness_left
  25. 0025rewrite hrd
  26. 0026simp
  27. 0027exists d
  28. 0028simp
  29. 0029cases zero_or_succ_right
  30. 0030exists x
  31. 0031exists S x1
  32. 0032split
  33. 0033rewrite IH_witness_witness_left
  34. 0034simp
  35. 0035exists x3
  36. 0036rewrite <- IH_witness_witness_right_witness
  37. 0037rewrite zero_or_succ_right_witness
  38. 0038simp [add_succ_left]