proposition: Lemma cyclemM : {in <[a]> & , {morph cyclem a : x y / x * y}}.
proof: Proof. by move=> x y ax ay; apply: expgMn; apply: (centsP (cycle_abelian a)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)