Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Proof.
intros n m p.
induction p.
Focus 2.
rewrite (mult_comm (n+m) (S p)).
rewrite (mult_comm n (S p)).
rewrite (mult_comm m (S p)).
simpl.
rewrite (mult_comm p (n + m)).
rewrite IHp.
rewrite <- (plus_assoc n (p*n) (m + p * m)).
rewrite (plus_comm (p * n) (m + p * m)).
rewrite (plus_assoc n (m + p * m) (p * n)).
rewrite (plus_assoc n m (p*m)).
rewrite (mult_comm n p).
rewrite (mult_comm m p).
rewrite (plus_comm (p * n) (p * m)).
rewrite (plus_assoc (n + m) (p*m) (p*n)).
reflexivity.






(* or just... *)

Require Import Omega.
Theorem mult_plus_distr_r : forall n m p : nat,
  (n + m) * p = (n * p) + (m * p).
Proof.
induction p; try omega; intuition.
Qed.