BT001K

lt_not_eq_add_middle

Stable · empty-context checked

A strict upper bound prevents the lower term from containing that bound as an additive middle block.

Exact expanded PA statement

forall r m a b. (exists k. k + S r = m) -> ~(r = (a + m) + b)

Structural proof guide

A strict upper bound prevents the lower term from containing that bound as an additive middle block.

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

Proof neighborhood

Direct dependencies

BT0001 add_succ_left

Direct dependents

BT001S positive_quotient_gap_impossible

Formal native tactic body

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

  1. 0001have hbad : forall z a w b. ~(z = (a + (w + S z)) + b)
  2. 0002intro z
  3. 0003induction z
  4. 0004intro a
  5. 0005intro w
  6. 0006intro b
  7. 0007intro hz
  8. 0008apply PA1
  9. 0009symm
  10. 0010rewrite PA4 at hz
  11. 0011rewrite PA4 at hz
  12. 0012specialize add_succ_left (a + (w + 0))
  13. 0013specialize add_succ_left b
  14. 0014rewrite add_succ_left at hz
  15. 0015exact hz
  16. 0016intro a
  17. 0017intro w
  18. 0018intro b
  19. 0019intro hz
  20. 0020specialize IH a
  21. 0021specialize IH w
  22. 0022specialize IH b
  23. 0023apply IH
  24. 0024apply PA2
  25. 0025rewrite PA4 at hz
  26. 0026rewrite PA4 at hz
  27. 0027specialize add_succ_left (a + (w + S z))
  28. 0028specialize add_succ_left b
  29. 0029rewrite add_succ_left at hz
  30. 0030exact hz
  31. 0031intro r
  32. 0032intro m
  33. 0033intro a
  34. 0034intro b
  35. 0035intro hr
  36. 0036intro heq
  37. 0037cases hr
  38. 0038specialize hbad r
  39. 0039specialize hbad a
  40. 0040specialize hbad x
  41. 0041specialize hbad b
  42. 0042apply hbad
  43. 0043rewrite <- hr_witness at heq
  44. 0044exact heq