Theorem imul_neutr

Proof
imul_neutr. ⊢ a ∈ ℤ → a⋅1 = a,
  pred_restr int_incl_in_real rmul_neutr.

Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, rmul_neutr.