proposition: Remark compl_of_typeF M U V (H := M`_\F) : H ><| U = M -> of_typeF M V -> of_typeF M U.
proof: Proof. move=> defM_U [[]]; rewrite -/H => ntH ntV defM part_b part_c. have oU: #|U| = #|V|. apply/eqP; rewrite -(@eqn_pmul2l #|H|) ?cardG_gt0 //. by rewrite (sdprod_card defM) (sdprod_card defM_U). have [x Mx defU]: exists2 x, x \in M & U :=: V :^ x. pose pi := \pi(V); have hallV: pi.-Hall(M) V. by rewrite Hall_pi // -(sdprod_Hall defM) (pHall_Hall (Fcore_Hall M)). apply: Hall_trans (hallV). rewrite mFT_sol // (sub_proper_trans _ (mFT_norm_proper ntH _)) ?gFnorm //. rewrite (proper_sub_trans _ (subsetT M)) // properEcard gFsub. by rewrite -(sdprod_card defM) ltn_Pmulr ?cardG_gt0 ?cardG_gt1. rewrite pHallE -(card_Hall hallV) oU eqxx andbT. by case/sdprod_context: defM_U. have nHx: x \in 'N(H) by apply: subsetP Mx; rewrite gFnorm. split; first by rewrite {1}defU conjsg_eq1. have [U1 [nsU1U abU1 prU1H]] := part_b. rewrite defU; exists (U1 :^ x)%G; split; rewrite ?normalJ ?abelianJ //. rewrite -/H -(normP nHx) -conjD1g => _ /imsetP[h Hh ->]. by rewrite -conjg_set1 normJ -conjIg conjSg prU1H. have [U0 [sU0V expU0 frobHU0]] := part_c. have [defHU0 _ ntU0 _ _] := Frobenius_context frobHU0. rewrite defU; exists (U0 :^ x)%G; split; rewrite ?conjSg ?exponentJ //. by rewrite -/H -(normP nHx) -conjYg FrobeniusJ. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection10) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)