proposition: Lemma mult_plus_distr2 : forall n m p : nat, n * (m + p) = n * m + n * p.
proof: Proof. intros. rewrite mult_sym. rewrite mult_plus_distr_r. rewrite mult_sym. replace (p * n) with (n * p). trivial with arith. apply mult_sym. Qed.
imports: Plus Mult Minus Lt Le Gt