Theorem nat_non_zero_is_succ

Proof
01. 1 ⊢ n ∈ ℕ, hypo.
02. 2 ⊢ ¬n = 0, hypo.
03. 1 ⊢ n = 0 ∨ ∃m. m ∈ ℕ ∧ n = m + 1, nat_zero_or_succ 1.
04. 1, 2 ⊢ ∃m. m ∈ ℕ ∧ n = m + 1, tollendo_ponens_right 3 2.
nat_non_zero_is_succ. ⊢ n ∈ ℕ → ¬n = 0 → ∃m. m ∈ ℕ ∧ n = m + 1,
  subj_intro_ii 4.

Dependencies
The given proof depends on eight axioms:
comp, efq, eq_refl, eq_subst, ext, radd_closed, real_is_set, subset.