proposition: Lemma Nmult_mult_assoc : forall n m x, (n * m) */ x == n */ (m */ x).
proof: Proof. intros n m x; induction n; intros; auto. simpl mult. rewrite (plus_Nmult_distr m (n * m) x). rewrite IHn; auto. Qed.
imports: ALEA(Utheory)