BT001G

le_or_lt

Stable · empty-context checked

Any two naturals satisfy weak order in one direction or strict order in the other.

Exact expanded PA statement

forall a b. (exists k. k + a = b) \/ exists k. k + S b = a

Structural proof guide

Any two naturals satisfy weak order in one direction or strict order in the other.

Direct prerequisites: none. The authored body proceeds by structural induction (2), case analysis (3), equality transport (2).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT00QS power_valuation_mul_upper BT00RC floor_sqrt_monotone BT00RF ceil_div_six_le_of_upper BT00SD eisenstein_initial_segment_indicator_choice BT00T8 choose_exists BT00XG division_double_quotient_bit BT00Y7 central_binom_prime_square_tail_valuation_le_one BT010B floor_sqrt_two_le_of_two_lt BT010E division_quotient_lower_of_scaled_le BT0117 factor_pair_has_small_member_below_square BT0124 bertrand_small_closed_upper BT0125 bertrand_closed_upper

Formal native tactic body

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

  1. 0001induction a
  2. 0002intro b
  3. 0003left
  4. 0004exists b
  5. 0005apply PA3
  6. 0006induction b
  7. 0007right
  8. 0008exists a
  9. 0009trans S (a + 0)
  10. 0010apply PA4
  11. 0011congr
  12. 0012apply PA3
  13. 0013specialize IH b
  14. 0014cases IH
  15. 0015left
  16. 0016cases IH_left
  17. 0017exists x
  18. 0018rewrite PA4
  19. 0019congr
  20. 0020exact IH_left_witness
  21. 0021right
  22. 0022cases IH_right
  23. 0023exists x
  24. 0024rewrite PA4
  25. 0025congr
  26. 0026exact IH_right_witness