proposition: Lemma set_Frobenius_compl G K H : K ><| H = G -> [Frobenius G with kernel K] -> [Frobenius G = K ><| H].
proof: Proof. move=> defG /Frobenius_kerP[ntK ltKG _ regKG]. apply/Frobenius_semiregularP=> //. by apply: contraTneq ltKG => H_1; rewrite -defG H_1 sdprodg1 properxx. apply: semiregular_sym => y /regKG sCyK. have [_ sHG _ _ tiKH] := sdprod_context defG. by apply/trivgP; rewrite /= -(setIidPr sHG) setIAC -tiKH setSI. 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)