proposition: Corollary Frobenius_sol_kernel_nil gT (G K H : {group gT}) : [Frobenius G = K ><| H] -> solvable G -> nilpotent K.
proof: Proof. move=> frobG solG; have [defG ntK ntH _ _] := Frobenius_context frobG. have{defG} /sdprodP[_ defG nKH tiKH] := defG. have[H1 | [p p_pr]] := trivgVpdiv H; first by case/eqP: ntH. case/Cauchy=> // x Hx ox; rewrite -ox in p_pr. have nKx: <[x]> \subset 'N(K) by rewrite cycle_subG (subsetP nKH). have tiKx: K :&: <[x]> = 1 by apply/trivgP; rewrite -tiKH setIS ?cycle_subG. apply: (prime_Frobenius_sol_kernel_nil (sdprodEY nKx tiKx)) => //. by rewrite (solvableS _ solG) // join_subG -mulG_subG -defG mulgS ?cycle_subG. by rewrite cent_cycle (Frobenius_reg_ker frobG) // !inE -order_gt1 prime_gt1. 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)