Theorem ile_compat_addl

Theorem. ile_compat_addl
a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a ≤ b → c + a ≤ c + b
Proof
ile_compat_addl. ⊢ a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a ≤ b → c + a ≤ c + b,
  pred_iii_restr int_incl_in_real rle_compat_addl.

Dependencies
The given proof depends on five axioms:
comp, eq_refl, eq_subst, radd_comm, rle_compat_add.