BT001O

division_remainder_succ

Stable · empty-context checked

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

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

Direct prerequisites: zero_add, add_succ_left, zero_or_succ. The authored body proceeds by structural induction (1), case analysis (6), intermediate claims (1), equality transport (7).

Proof neighborhood

Direct dependencies

BT0000 zero_add BT0001 add_succ_left BT000Q zero_or_succ

Direct dependents

BT001P division_remainder_exists

Formal native tactic body

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

  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]