Theorem imul_distr_add

Proof
imul_distr_add. ⊢ a ∈ ℤ → b ∈ ℤ → c ∈ ℤ → (a + b)⋅c = a⋅c + b⋅c,
  pred_iii_restr int_incl_in_real rmul_distr_add.

Dependencies
The given proof depends on six axioms:
comp, eq_refl, eq_subst, radd_closed, rmul_comm, rmul_distl_add.