proposition: Lemma plus_Nmult_distr : forall n m x, (n + m) */ x== (n */ x) + (m */ x).
proof: Proof. intros n m x; induction n; auto; intros. rewrite plus_Sn_m. rewrite (Nmult_S (n + m) x). setoid_rewrite IHn. rewrite (Nmult_S n x); auto. Qed.
imports: ALEA(Utheory)