Theorem imul_distl_add

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

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