proposition: Lemma cyclicY K H : cyclic K -> cyclic H -> H \subset 'C(K) -> coprime #|K| #|H| -> cyclic (K <*> H).
proof: Proof. by move=> cycK cycH cKH coKH; rewrite cent_joinEr // cyclicM. 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)