proposition: Lemma Frobenius_normal_proper_ker N : [Frobenius G = K ><| R] -> solvable K -> N <| G -> ~~ (K \subset N) -> N \proper K.
proof: Proof. move=> frobG solK nsNG ltNK; have [sNG nNG] := andP nsNG; pose H := N :&: K. have [defG _ ntR _ _] := Frobenius_context frobG. have [nsKG _ /mulG_sub[sKG _] nKR tiKR] := sdprod_context defG. have nsHG: H <| G := normalI nsNG nsKG; have [_ nHG] := andP nsHG. have ltHK: H \proper K by rewrite /proper subsetIr subsetI subxx andbT. suffices /eqP tiNR: N :&: R == 1. rewrite /proper ltNK andbT -(setIidPl sNG). rewrite -(cover_partition (Frobenius_partition frobG)) big_distrr /=. apply/bigcupsP=> _ /setU1P[->| /imsetP[x Kx ->]]; first exact: subsetIr. rewrite conjD1g setIDA subDset -(normsP (subset_trans sKG nNG) x) //. by rewrite -conjIg tiNR conjs1g subsetUl. suffices: (N :&: R) / H \subset [1]. by rewrite -subG1 quotient_sub1 ?normsGI // -subsetIidr setIACA tiKR setIg1. have frobGq := Frobenius_proper_quotient frobG solK nsHG ltHK. have [_ ntKq _ _ _] := Frobenius_context frobGq. rewrite -(cent_semiregular (Frobenius_reg_compl frobGq) _ ntKq) //. rewrite subsetI quotientS ?subsetIr // quotient_cents2r //. by rewrite commg_subI ?setIS // subsetIidl (subset_trans sKG). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype tuple bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action commutator gproduct) mathcomp(zmodp cyclic gfunctor center pgroup gseries nilpotent sylow) mathcomp(finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(wielandt_fixpoint BGsection1 BGsection2)