BT000K

le_total

Stable · empty-context checked

Every pair of natural numbers is comparable in the defined order.

Exact expanded PA statement

forall n m. n <= m \/ m <= n

Structural proof guide

Every pair of natural numbers is comparable in the defined order.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

BT001U division_remainder_unique BT00VY no_bertrand_central_prime_divisor_le BT00W2 no_bertrand_central_prime_divisor_ranges BT0117 factor_pair_has_small_member_below_square

Formal native tactic body

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

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