Theorem nat_non_negative

Proof
01. ⊢ 0 ≤ 0, calc.
02. 2 ⊢ n ∈ ℕ, hypo.
03. 3 ⊢ 0 ≤ n, hypo.
04. ⊢ 0 ∈ ℝ, calc.
05. 2 ⊢ n ∈ ℝ, incl_elim nat_incl_in_real 2.
06. ⊢ 1 ∈ ℝ, calc.
07. 2, 3 ⊢ 0 + 1 ≤ n + 1, rle_compat_add 4 5 6 3.
08. ⊢ 0 ≤ 0 + 1, calc.
09. ⊢ 0 + 1 ∈ ℝ, calc.
10. 2 ⊢ n + 1 ∈ ℝ, radd_closed 5 6.
11. 2, 3 ⊢ 0 ≤ n + 1, rle_trans 4 9 10 8 7.
12. ⊢ n ∈ ℕ → 0 ≤ n → 0 ≤ n + 1, subj_intro_ii 11.
13. ⊢ ∀n. n ∈ ℕ → 0 ≤ n → 0 ≤ n + 1, uq_intro 12.
14. ⊢ ∀n. n ∈ ℕ → 0 ≤ n,
  nat_induction 1 13, P n ↔ 0 ≤ n.
nat_non_negative. ⊢ n ∈ ℕ → 0 ≤ n, uq_elim 14.

Dependencies
The given proof depends on nine axioms:
comp, eq_refl, eq_subst, ext, radd_closed, real_is_set, rle_compat_add, rle_trans, subset.