proposition: Lemma cyc_imp_comm: forall (M:CMonoid)(H:(cyclic M)), (commutes (@csg_op M)).
proof: Proof. intros M H. unfold commutes. intros x y. unfold cyclic in H. elim H. clear H. intros c0 H. elim (H x). intros nx Hx. elim (H y). intros ny Hy. rewrite <- Hx. rewrite <- Hy. rewrite <- (power_plus M c0 nx ny). replace (nx+ny) with (ny+nx). rewrite -> (power_plus M c0 ny nx). now apply eq_reflexive. intuition. Qed.
imports: Coq.Arith.Euclid CoRN.model.Zmod.Cmod CoRN.algebra.CSemiGroups CoRN.tactics.csetoid_rewrite CoRN.model.structures.Nsec CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms