proposition: Lemma Frobenius_semiregularP G K H : K ><| H = G -> K :!=: 1 -> H :!=: 1 -> reflect (semiregular K H) [Frobenius G = K ><| H].
proof: Proof. move=> defG ntK ntH. apply: (iffP idP) => [|regG]; first exact: Frobenius_reg_ker. have [nsKG sHG defKH nKH tiKH]:= sdprod_context defG; have [sKG _]:= andP nsKG. apply/and3P; split; first by rewrite defG. by rewrite eqEcard sHG -(sdprod_card defG) -ltnNge ltn_Pmull ?cardG_gt1. apply/normedTI_memJ_P; rewrite setD_eq0 subG1 sHG -defKH -(normC nKH). split=> // z _ /setD1P[ntz Hz] /mulsgP[y x Hy Kx ->]; rewrite groupMl // !inE. rewrite conjg_eq1 ntz; apply/idP/idP=> [Hzxy | Hx]; last by rewrite !in_group. apply: (subsetP (sub1G H)); have Hzy: z ^ y \in H by apply: groupJ. rewrite -(regG (z ^ y)); last by apply/setD1P; rewrite conjg_eq1. rewrite inE Kx cent1C (sameP cent1P commgP) -in_set1 -[[set 1]]tiKH inE /=. rewrite andbC groupM ?groupV -?conjgM //= commgEr groupMr //. by rewrite memJ_norm ?(subsetP nKH) ?groupV. 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)