proposition: Lemma Frobenius_proper_quotient N : [Frobenius G = K ><| R] -> solvable K -> N <| G -> N \proper K -> [Frobenius G / N = (K / N) ><| (R / N)].
proof: Proof. move=> frobG solK nsNG /andP[sNK ltNK]. have [defG _ ntR _ _] := Frobenius_context frobG. have [nsKG sRG defKR nKR tiKR] := sdprod_context defG; have [sKG _]:= andP nsKG. have nsNK := normalS sNK sKG nsNG. apply/Frobenius_semiregularP=> [|||Nx]. - rewrite sdprodE ?quotient_norms //. by rewrite -quotientMl ?defKR ?normal_norm. by rewrite -quotientGI // tiKR quotient1. - by rewrite -subG1 quotient_sub1 ?normal_norm. - rewrite -subG1 quotient_sub1; last by rewrite (subset_trans sRG) ?normal_norm. apply: contra ntR => sRN. by rewrite -subG1 -tiKR subsetI (subset_trans sRN) /=. rewrite !inE andbC => /andP[/morphimP[x nNx Rx ->{Nx}] notNx]. apply/trivgP; rewrite /= -cent_cycle -quotient_cycle //. rewrite -coprime_quotient_cent ?cycle_subG //; last first. by apply: coprimegS (Frobenius_coprime frobG); rewrite cycle_subG. rewrite cent_cycle (Frobenius_reg_ker frobG) ?quotient1 // !inE Rx andbT. by apply: contraNneq notNx => ->; rewrite morph1. 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)