proposition: Lemma Frobenius_quotient N : [Frobenius G = K ><| R] -> solvable K -> N <| G -> ~~ (K \subset N) -> [Frobenius G / N = (K / N) ><| (R / N)].
proof: Proof. move=> frobG solK nsNG ltKN; apply: Frobenius_proper_quotient => //. exact: (Frobenius_normal_proper_ker frobG). 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)