proposition: Lemma cycleM a b : commute a b -> coprime #[a] #[b] -> <[a * b]> = <[a]> * <[b]>.
proof: Proof. move=> cab co_ab; apply/eqP; rewrite eqEsubset -(cent_joinEl (cents_cycle cab)). rewrite join_subG {3}cab !cycleMsub // 1?coprime_sym //. by rewrite -genM_join cycle_subG mem_gen // imset2_f ?cycle_id. 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)