proposition: Lemma cycleMsub a b : commute a b -> coprime #[a] #[b] -> <[a]> \subset <[a * b]>.
proof: Proof. move=> cab co_ab; apply/subsetP=> _ /cycleP[k ->]. apply/cycleP; exists (chinese #[a] #[b] k 0); symmetry. rewrite expgMn // -expg_mod_order chinese_modl // expg_mod_order. by rewrite /chinese addn0 -mulnA mulnCA expgM expg_order expg1n mulg1. 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)