proposition: Lemma nmult_mult : forall n m x, nmult (nmult x m) n [=] nmult x (m * n).
proof: Proof. simple induction n. intro. rewrite Nat.mul_0_r. algebra. clear n; intros. simpl in |- *. rewrite Nat.mul_comm. simpl in |- *. eapply eq_transitive_unfolded. 2: apply nmult_plus. rewrite Nat.mul_comm. algebra. Qed.
imports: CoRN.algebra.CGroups