proposition: Lemma cyclicM A B : cyclic A -> cyclic B -> B \subset 'C(A) -> coprime #|A| #|B| -> cyclic (A * B).
proof: Proof. move=> /cyclicP[a ->] /cyclicP[b ->]; rewrite cent_cycle cycle_subG => cab coab. by rewrite -cycleM ?cycle_cyclic //; apply/esym/cent1P. 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)