Theorem nle_compat_add

Proof
nle_compat_add. ⊢ a ∈ ℕ → b ∈ ℕ → c ∈ ℕ → a ≤ b → a + c ≤ b + c,
  pred_iii_restr nat_incl_in_real rle_compat_add.

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