proposition: Lemma generator_imp_cyclic: (forall (u:M), (is_generator M u)-> (cyclic M)):CProp.
proof: Proof. intros u H. unfold is_generator in H. exists u. exact H. 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