BT0097

lt_three_cases

Stable · empty-context checked

Every natural strictly below three is zero, one, or two.

Exact expanded PA statement

forall x. (exists h. h + S x = 3) -> x = 0 \/ x = 1 \/ x = 2

Structural proof guide

Every natural strictly below three is zero, one, or two.

Direct prerequisites: le_of_succ_le_succ, le_eq_or_lt, le_zero. The authored body proceeds by case analysis (2), intermediate claims (5).

Proof neighborhood

Direct dependencies

BT0017 le_of_succ_le_succ BT001C le_eq_or_lt BT000Y le_zero

Direct dependents

BT010B floor_sqrt_two_le_of_two_lt

Formal native tactic body

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

  1. 0001intro x
  2. 0002intro hb
  3. 0003have hle2 : exists h. h + x = 2
  4. 0004specialize le_of_succ_le_succ x
  5. 0005specialize le_of_succ_le_succ 2
  6. 0006apply le_of_succ_le_succ
  7. 0007exact hb
  8. 0008have hc2 : x = 2 \/ exists h. h + S x = 2
  9. 0009specialize le_eq_or_lt x
  10. 0010specialize le_eq_or_lt 2
  11. 0011apply le_eq_or_lt
  12. 0012exact hle2
  13. 0013cases hc2
  14. 0014right
  15. 0015exact hc2_left
  16. 0016left
  17. 0017have hle1 : exists h. h + x = 1
  18. 0018specialize le_of_succ_le_succ x
  19. 0019specialize le_of_succ_le_succ 1
  20. 0020apply le_of_succ_le_succ
  21. 0021exact hc2_right
  22. 0022have hc1 : x = 1 \/ exists h. h + S x = 1
  23. 0023specialize le_eq_or_lt x
  24. 0024specialize le_eq_or_lt 1
  25. 0025apply le_eq_or_lt
  26. 0026exact hle1
  27. 0027cases hc1
  28. 0028right
  29. 0029exact hc1_left
  30. 0030left
  31. 0031have hle0 : exists h. h + x = 0
  32. 0032specialize le_of_succ_le_succ x
  33. 0033specialize le_of_succ_le_succ 0
  34. 0034apply le_of_succ_le_succ
  35. 0035exact hc1_right
  36. 0036specialize le_zero x
  37. 0037apply le_zero
  38. 0038exact hle0