proposition: Lemma cyclic_dprod K H G : K \x H = G -> cyclic K -> cyclic H -> cyclic G = coprime #|K| #|H| .
proof: Proof. case/dprodP=> _ defKH cKH tiKH cycK cycH; pose m := lcmn #|K| #|H|. apply/idP/idP=> [/cyclicP[x defG] | coKH]; last by rewrite -defKH cyclicM. rewrite /coprime -dvdn1 -(@dvdn_pmul2l m) ?lcmn_gt0 ?cardG_gt0 //. rewrite muln_lcm_gcd muln1 -TI_cardMg // defKH defG order_dvdn. have /mulsgP[y z Ky Hz ->]: x \in K * H by rewrite defKH defG cycle_id. rewrite -[1]mulg1 expgMn; last exact/commute_sym/(centsP cKH). apply/eqP; congr (_ * _); apply/eqP; rewrite -order_dvdn. exact: dvdn_trans (order_dvdG Ky) (dvdn_lcml _ _). exact: dvdn_trans (order_dvdG Hz) (dvdn_lcmr _ _). 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)