Theorem nmul_neutl

Proof
nmul_neutl. ⊢ a ∈ ℕ → 1⋅a = a,
  pred_restr nat_incl_in_real rmul_neutl.

Dependencies
The given proof depends on seven axioms:
comp, eq_refl, eq_subst, radd_closed, real_is_set, rmul_comm, rmul_neutr.