Theorem nat_succ_non_zero

Proof
01. 1 ⊢ n ∈ ℕ, hypo.
02. 2 ⊢ n + 1 = 0, hypo.
03. 1 ⊢ 0 ≤ n, nat_non_negative 1.
04. 1 ⊢ n ∈ ℝ, incl_elim nat_incl_in_real 1.
05. ⊢ 0 ∈ ℝ, calc.
06. ⊢ 1 ∈ ℝ, calc.
07. 1 ⊢ 0 + 1 ≤ n + 1, rle_compat_add 5 4 6 3.
08. ⊢ 1 = 0 + 1, calc.
09. 1 ⊢ 1 ≤ n + 1, eq_le_trans 8 7.
10. 1, 2 ⊢ 1 ≤ 0, le_eq_trans 9 2.
11. ⊢ ¬1 ≤ 0, calc.
12. 1, 2 ⊢ ⊥, neg_elim 11 10.
13. 1 ⊢ ¬(n + 1 = 0), neg_intro 12.
nat_succ_non_zero. ⊢ n ∈ ℕ → ¬(n + 1 = 0), subj_intro 13.

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.