proposition: Lemma Frobenius_reg_ker : semiregular K H.
proof: Proof. move=> x /setD1P[ntx Hx]. apply/trivgP/subsetP=> y /setIP[Ky cxy]; apply: contraR ntx => nty. have K1y: y \in K^# by rewrite inE nty. have [/eqP/sdprod_context[_ sHG _ _ tiKH] _] := andP frobG. suffices: x \in K :&: H by rewrite tiKH inE. by rewrite inE (subsetP (Frobenius_cent1_ker K1y)) // inE cent1C (subsetP sHG). 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)