proposition: Lemma bounded_proper_coherent H1 : H1 <| M -> H1 \proper HU -> coherent (S_ H1) M^# tau -> (#|HU : H1| <= 2 * q * #|U : C| + 1)%N.
proof: Proof. move=> nsH1_M psH1_M' cohH1; have [nsHHU _ _ _ _] := sdprod_context defHU. suffices: #|HU : H1|%:R - 1 <= 2%:R * #|M : HC|%:R * sqrtC #|HC : HC|%:R :> algC. rewrite indexgg sqrtC1 mulr1 -leC_nat natrD -lerBlDr -mulnA natrM. congr (_ <= _ * _%:R); apply/eqP; rewrite -(eqn_pmul2l (cardG_gt0 HC)). rewrite Lagrange ?normal_sub // mulnCA -(dprod_card defHC) -mulnA mulnC. by rewrite Lagrange ?subsetIl // (sdprod_card defHU) (sdprod_card defM). apply/negP/(coherent_seqIndD_bound _ _ scoh1 _ _ _ FTtype34_noncoherence) => //. suffices /center_idP->: abelian (HC / H0C) by rewrite genS ?setSU. suffices /isog_abelian<-: Hbar \isog HC / H0C by apply: abelem_abelian abelHbar. by rewrite /= [`H0C]joingC quotient_sdprodr_isog ?(dprodWsdC defHC). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10)