Theorem ilt_add_cancel_rr

Theorem. ilt_add_cancel_rr
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a + c < b + c → a < b
Proof
ilt_add_cancel_rr. ⊢ a ∈ ℤ → b ∈ ℤ → c ∈ ℤ →
  a + c < b + c → a < b,
  pred_iii_restr int_incl_in_real rlt_add_cancel_rr.

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