Theorem nle_lt_tricho

Proof
nle_lt_tricho. ⊢ a ∈ ℕ → b ∈ ℕ → a ≤ b ∨ b < a,
  pred_ii_restr nat_incl_in_real rle_lt_tricho.

Dependencies
The given proof depends on nine axioms:
comp, efq, eq_refl, eq_subst, lem, radd_closed, real_is_set, rle_refl, rle_total.