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