proposition: Lemma Dade_setU1 : {in calP & A, forall B a, 'H(a |: B) = 'C_('H(B))[a]}.
proof: Proof. move=> B a dB Aa; rewrite /'H(_) bigcap_setU big_set1 -/'H(B). apply/eqP; rewrite setIC eqEsubset setIS // subsetI subsetIl /=. have [sHBG pi'HB]: 'H(B) \subset G /\ pi^'.-group 'H(B). have [sBA /set0Pn[b Bb]] := setIdP dB; have Ab := subsetP sBA b Bb. have sHBb: 'H(B) \subset H b by rewrite ['H(B)](bigD1 b) ?subsetIl. by rewrite (pgroupS sHBb) ?pi'H ?(subset_trans sHBb) ?sHG. have [nsHa _ defCa _ _] := sdprod_context (defCA Aa). have [hallHa _] := coprime_mulGp_Hall defCa (pi'H a) (piCL Aa). by rewrite (sub_normal_Hall hallHa) ?(pgroupS (subsetIl _ _)) ?setSI. Qed.
imports: HB(structures) 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 zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius ssrnum) mathcomp(matrix mxalgebra mxrepresentation vector algC classfun character) mathcomp(inertia vcharacter) odd_order(PFsection1)