proposition: Lemma FTtype34_der2 : M^`(2)%g = HC.
proof: Proof. have [defFM [_ not_cHU] _ _] := typeP_context MtypeP. have [_ sW1M _ _ tiHU_W1] := sdprod_context defM. have{defFM} sM''_HC: M^`(2)%g \subset HC. by rewrite -defHC defFM; have [_ _ []] := MtypeP. have scohM'': subcoherent (S_ M^`(2)) tau R. exact/(subset_subcoherent scoh1)/seqInd_conjC_subset1. have cohM'': coherent (S_ M^`(2)) M^# tau. apply: uniform_degree_coherence scohM'' _. apply: all_pred1_constant #|M : HU|%:R _ _; rewrite all_map. apply/allP=> _ /seqIndP[s /setDP[kerM'' _] ->] /=; rewrite inE in kerM''. by rewrite cfInd1 ?gFsub // lin_char1 ?mulr1 ?lin_irr_der1. have ubHC: (#|HC : M^`(2)| < 2 * q + 1)%N. rewrite -(ltn_pmul2r (indexg_gt0 U C)) mulnDl mul1n. apply: leq_ltn_trans (_ : 2 * q * #|U : C| + 1 < _)%N; last first. by rewrite ltn_add2l indexg_gt1 subsetIidl not_cHU //; have [] := Mtype24. have {1}->: #|U : C| = #|HU : HC| by apply: index_sdprodr (subsetIl _ _). by rewrite mulnC (Lagrange_index sHC_HU) // bounded_proper_coherent ?gFnormal. have regHC_W1: semiregular (HC / M^`(2)) (W1 / M^`(2)). by apply: semiregularS (Frobenius_reg_ker frobMtilde); rewrite quotientS. suffices /dvdnP[k Dk]: 2 * q %| #|HC : M^`(2)|.-1. apply: contraTeq ubHC; rewrite -leqNgt eqEsubset sM''_HC -indexg_gt1 addn1. by rewrite -[#|_:_|]prednK // {}Dk !ltnS muln_gt0 => /andP[/leq_pmull->]. rewrite Gauss_dvd; last by rewrite coprime2n mFT_odd. rewrite dvdn2 -subn1 oddB // addbT negbK subn1. rewrite -card_quotient; last by rewrite (subset_trans sHC_HU) // (der_norm 1). have Dq: q = #|W1 / M^`(2)|%g. apply/card_isog/quotient_isog; first by rewrite (subset_trans sW1M) ?gFnorm. by apply/trivgP; rewrite -tiHU_W1 setSI // (der_sub 1). rewrite quotient_odd ?mFT_odd //= Dq regular_norm_dvd_pred ?quotient_norms //. by rewrite (subset_trans sW1M) ?normal_norm. 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)