proposition: Lemma Frobenius_subl G K K1 H : K1 :!=: 1 -> K1 \subset K -> H \subset 'N(K1) -> [Frobenius G = K ><| H] -> [Frobenius K1 <*> H = K1 ><| H].
proof: Proof. move=> ntK1 sK1K nK1H frobG; have [_ _ ntH _ _] := Frobenius_context frobG. apply/Frobenius_semiregularP=> //. by rewrite sdprodEY ?coprime_TIg ?(coprimeSg sK1K) ?(Frobenius_coprime frobG). by move=> x /(Frobenius_reg_ker frobG) cKx1; apply/trivgP; rewrite -cKx1 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)