BT001S

positive_quotient_gap_impossible

Stable · empty-context checked

A positive gap between quotients makes two bounded-remainder decompositions unequal.

Exact expanded PA statement

forall m q q2 r s k. (exists z. z + S r = m) -> S k + q = q2 -> ~(m * q + r = m * q2 + s)

Structural proof guide

A positive gap between quotients makes two bounded-remainder decompositions unequal.

Direct prerequisites: add_comm, add_assoc, mul_add, add_left_cancel, lt_not_eq_add_middle. The authored body proceeds by equality transport (4).

Proof neighborhood

Direct dependencies

BT0002 add_comm BT0003 add_assoc BT0007 mul_add BT000V add_left_cancel BT001K lt_not_eq_add_middle

Direct dependents

BT001U division_remainder_unique

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 q
  3. 0003intro q2
  4. 0004intro r
  5. 0005intro s
  6. 0006intro k
  7. 0007intro hr
  8. 0008intro hgap
  9. 0009intro heq
  10. 0010specialize lt_not_eq_add_middle r
  11. 0011specialize lt_not_eq_add_middle m
  12. 0012specialize lt_not_eq_add_middle (m * k)
  13. 0013specialize lt_not_eq_add_middle s
  14. 0014apply lt_not_eq_add_middle
  15. 0015exact hr
  16. 0016specialize add_left_cancel (m * q)
  17. 0017specialize add_left_cancel r
  18. 0018specialize add_left_cancel ((m * k + m) + s)
  19. 0019apply add_left_cancel
  20. 0020trans m * q2 + s
  21. 0021exact heq
  22. 0022rewrite <- hgap
  23. 0023specialize add_comm S k
  24. 0024specialize add_comm q
  25. 0025rewrite add_comm
  26. 0026specialize mul_add m
  27. 0027specialize mul_add q
  28. 0028specialize mul_add S k
  29. 0029rewrite mul_add
  30. 0030rewrite PA6
  31. 0031specialize add_assoc (m * q)
  32. 0032specialize add_assoc (m * k + m)
  33. 0033specialize add_assoc s
  34. 0034apply add_assoc