Theorem nle_compat_addl

Proof
nle_compat_addl. ⊢ a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a ≤ b → c + a ≤ c + b,
  pred_iii_restr nat_incl_in_real rle_compat_addl.

Dependencies
The given proof depends on six axioms:
comp, eq_subst, radd_closed, radd_comm, real_is_set, rle_compat_add.