Theorem ile_compat_add

Proof
ile_compat_add. ⊢ a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → a ≤ b → a + c ≤ b + c,
  pred_iii_restr int_incl_in_real rle_compat_add.

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