proposition: Lemma Frobenius_subr G K H H1 : H1 :!=: 1 -> H1 \subset H -> [Frobenius G = K ><| H] -> [Frobenius K <*> H1 = K ><| H1].
proof: Proof. move=> ntH1 sH1H frobG; have [defG ntK _ _ _] := Frobenius_context frobG. apply/Frobenius_semiregularP=> //. have [_ _ /(subset_trans sH1H) nH1K tiHK] := sdprodP defG. by rewrite sdprodEY //; apply/trivgP; rewrite -tiHK setIS. by apply: sub_in1 (Frobenius_reg_ker frobG); apply/subsetP/setSD. 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)