Theorem nsub_zero

Proof
nsub_zero. ⊢ a ∈ ℕ → a - 0 = a,
  pred_restr nat_incl_in_real rsub_zero.

Dependencies
The given proof depends on six axioms:
comp, eq_refl, eq_subst, radd_closed, radd_neutr, real_is_set.