proposition: Lemma nmult_plus : forall m n x, nmult x m[+]nmult x n [=] nmult x (m + n).
proof: Proof. simple induction m. simpl in |- *; algebra. clear m; intro m. intros. simpl in |- *. Step_final (x[+](nmult x m[+]nmult x n)). Qed.
imports: CoRN.algebra.CGroups