nat_succ

Theorem nat_succ_inj

Theorem. nat_succ_inj
a ∈ ℕ → b ∈ ℕ → a + 1 = b + 1 → a = b

Proof
01. 1 ⊢ a ∈ ℕ, hypo.
02. 2 ⊢ b ∈ ℕ, hypo.
03. 3 ⊢ a + 1 = b + 1, hypo.
04. 1 ⊢ a ∈ ℝ, incl_elim nat_incl_in_real 1.
05. 2 ⊢ b ∈ ℝ, incl_elim nat_incl_in_real 2.
06. ⊢ 1 ∈ ℝ, calc.
07. 1, 2, 3 ⊢ a = b, radd_cancel_rr 4 5 6 3.
nat_succ_inj. ⊢ a ∈ ℕ → b ∈ ℕ → a + 1 = b + 1 → a = b,
  subj_intro_iii 7.

Dependencies
The given proof depends on nine axioms:
comp, eq_refl, eq_subst, radd_assoc, radd_closed, radd_inv, radd_neutr, real_is_set, rneg_closed.