proposition: Lemma restr_Dade_hyp : Dade_hypothesis G L A1.
proof: Proof. have [/andP[sAL nAL] notA_1 sLG conjAG [H defCa coHL]] := ddA. have nsA1L: A1 <| L by rewrite /normal (subset_trans sA1A). split; rewrite ?(contra (@ssA1A _)) //; first exact: sub_in2 conjAG. by exists H; [apply: sub_in1 defCa | apply: sub_in2 coHL]. 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)