proposition: Lemma FTtypeP_nonGalois_facts : ~~ typeP_Galois StypeP -> q = 3%N /\ u = (p.-1./2 ^ 2)%N.
proof: Proof. move=> gal'S; have: has irrIndH calS. by apply: contraR gal'S => /(FTtypeP_no_Ind_Fitting_facts maxS StypeP)[]. by case/hasP=> lambda Slam /FTtypeP_Ind_Fitting_nonGalois_facts; apply. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct center cyclic commutator gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum rat algC cyclotomic algnum) mathcomp(classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9) odd_order(PFsection10 PFsection11 PFsection12)