nle_lt_trans

Theorem. nle_lt_trans
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a ≤ b → b < c → a < c

Proof
nle_lt_trans. ⊢ a ∈ ℕ → b ∈ ℕ → c ∈ ℕ →
  a ≤ b → b < c → a < c,
  pred_iii_restr nat_incl_in_real rle_lt_trans.

Dependencies
The given proof depends on seven axioms:
comp, eq_refl, eq_subst, radd_closed, real_is_set, rle_antisym, rle_trans.