proposition: Lemma nmult_wd : forall (x y:G) (n m:nat), (x [=] y) -> n = m -> nmult x n [=] nmult y m.
proof: Proof. simple induction n; intros. rewrite <- H0; algebra. rewrite <- H1; simpl in |- *; algebra. Qed.
imports: CoRN.algebra.CGroups