proposition: Lemma prime_FrobeniusP G K H : K :!=: 1 -> prime #|H| -> reflect (K ><| H = G /\ 'C_K(H) = 1) [Frobenius G = K ><| H].
proof: Proof. move=> ntK H_pr; have ntH: H :!=: 1 by rewrite -cardG_gt1 prime_gt1. have [defG | not_sdG] := eqVneq (K ><| H) G; last first. by apply: (iffP andP) => [] [defG]; rewrite defG ?eqxx in not_sdG. apply: (iffP (Frobenius_semiregularP defG ntK ntH)) => [regH | [_ regH x]]. split=> //; have [x defH] := cyclicP (prime_cyclic H_pr). by rewrite defH cent_cycle regH // !inE defH cycle_id andbT -cycle_eq1 -defH. case/setD1P=> nt_x Hx; apply/trivgP; rewrite -regH setIS //= -cent_cycle. by rewrite centS // prime_meetG // (setIidPr _) ?cycle_eq1 ?cycle_subG. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)