fact: Definition is_generator (M:CMonoid)(u:M):CProp:= forall (m:M),{n:nat | (power_CMonoid u n)[=]m}.
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