(* Exercise coq_nat_10 *)

(* Multiplication distributes over addition *)

Require Import Arith.

Lemma mult_plus_distr : forall m n p, m * (n + p) = m * n + m * p.

Proof.
intros.
induction m.
- auto.
- simpl.
  rewrite IHm.
  rewrite plus_assoc.
  rewrite plus_assoc.
(* The goal now is, with all brackets put in:
     (((n + p) + m * n) + m * p) = (((n + m * n) + p) + m * p)
 *)
  rewrite <- (plus_assoc n p (m*n)).
  rewrite <- (plus_assoc n (m*n) p).
  rewrite (plus_comm (m * n) p).
  reflexivity.
Qed.