PA002D

positive_quotient_gap_impossible

Stable checked-use theorem · independently closed

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

Generated structural guide

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

Use the direct prerequisites add_comm, add_assoc, mul_add, add_left_cancel, lt_not_eq_add_middle as previously established PA formulas.

The proof proceeds by equality transport (4).

Referenced ingredients

PA000F add_comm PA0009 add_assoc PA000A mul_add PA002B add_left_cancel PA002C lt_not_eq_add_middle

Proof neighborhood

Direct dependencies

PA000F add_comm PA0009 add_assoc PA000A mul_add PA002B add_left_cancel PA002C lt_not_eq_add_middle

Direct dependents

PA002E division_remainder_unique

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