proposition: Remark compl_of_typeII_IV : FTtype M != 5%N -> of_typeII_IV M U defW.
proof: Proof. move=> Mtype'5. have [Ux Wx W1x W2x defWx Mtype24]: exists_typeP (of_typeII_IV M). have:= FTtype_range M; rewrite leq_eqVlt eq_sym (leq_eqVlt _ 5). rewrite (negPf FTtypeP_neq1) (negPf Mtype'5) /= -mem_iota !inE. by case/or3P=> /FTtypeP[]// Ux Wx W1x W2x dWx []; exists Ux Wx W1x W2x dWx. have [MtypePx ntUx prW1x tiFM] := Mtype24. have [x [Mx defUx defW1x _ _]] := of_typeP_conj MtypePx. by rewrite -defUx -defW1x cardJg conjsg_eq1 in ntUx prW1x. 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)