Theorem imul_comm

Proof
imul_comm. ⊢ a ∈ ℤ → b ∈ ℤ → a⋅b = b⋅a,
  pred_ii_restr int_incl_in_real rmul_comm.

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