proposition: Lemma Nmult_Uplus_distr : forall n x y, n */ (x + y) == (n */ x) + (n */ y).
proof: Proof. intros n x y; induction n. simpl; auto. rewrite (Nmult_S n (x+y)). rewrite IHn. norm_assoc_right. rewrite (Uplus_perm2 y (n */ x) (n */ y)). rewrite <- (Nmult_S n y). norm_assoc_left. apply Uplus_eq_compat; auto. Qed.
imports: ALEA(Utheory)