Theorem nlt_add_cancel_rr

Theorem. nlt_add_cancel_rr
a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a + c < b + c → a < b
Proof
nlt_add_cancel_rr. ⊢ a ∈ ℕ → b ∈ ℕ → c ∈ ℕ →
  a + c < b + c → a < b,
  pred_iii_restr nat_incl_in_real rlt_add_cancel_rr.

Dependencies
The given proof depends on 10 axioms:
comp, eq_refl, eq_subst, radd_assoc, radd_closed, radd_inv, radd_neutr, real_is_set, rle_compat_add, rneg_closed.