proposition: Lemma rank2_SCN3_empty gT p (R : {group gT}) : p.-group R -> odd #|R| -> ('r(R) <= 2) = ('SCN_3(R) == set0).
proof: Proof. move=> pR oddR; apply/idP/idP=> [leR2 | SCN_3_empty]. apply/set0Pn=> [[A /setIdP[/SCN_P[/andP[sAR _] _]]]]. by rewrite ltnNge (leq_trans (rankS sAR)). rewrite (rank_pgroup pR) leqNgt; apply/negP=> gtR2. have ncycR: ~~ cyclic R by rewrite (odd_pgroup_rank1_cyclic pR) // -ltnNge ltnW. have{ncycR} [Z nsZR] := ex_odd_normal_p2Elem pR oddR ncycR. case/pnElemP=> sZR abelZ dimZ2; have [pZ cZZ _] := and3P abelZ. have{SCN_3_empty} defZ: 'Ohm_1('C_R(Z)) = Z. apply: (Ohm1_cent_max_normal_abelem _ pR). by have:= oddSg sZR oddR; rewrite (card_pgroup pZ) dimZ2 oddX. apply/maxgroupP; split=> [|H /andP[nsHR abelH] sZH]; first exact/andP. have [pH cHH _] := and3P abelH; apply/eqP; rewrite eq_sym eqEproper sZH /=. pose normal_abelian := [pred K : {group gT} | K <| R & abelian K]. have [|K maxK sHK] := @maxgroup_exists _ normal_abelian H; first exact/andP. apply: contraL SCN_3_empty => ltZR; apply/set0Pn; exists K. rewrite inE (max_SCN pR) {maxK}//= -dimZ2 (leq_trans _ (rankS sHK)) //. by rewrite (rank_abelem abelH) properG_ltn_log. have{gtR2} [A] := p_rank_geP gtR2; pose H := 'C_A(Z); pose K := H <*> Z. case/pnElemP=> sAR abelA dimA3; have [pA cAA _] := and3P abelA. have{nsZR} nZA := subset_trans sAR (normal_norm nsZR). have sHA: H \subset A := subsetIl A _; have abelH := abelemS sHA abelA. have geH2: logn p #|H| >= 2. rewrite -ltnS -dimA3 -(Lagrange sHA) lognM // -addn1 leq_add2l /= -/H. by rewrite logn_quotient_cent_abelem ?dimZ2. have{abelH} abelK : p.-abelem K. by rewrite (cprod_abelem _ (cprodEY _)) 1?centsC ?subsetIr ?abelH. suffices{sZR cZZ defZ}: 'r(Z) < 'r(K). by rewrite ltnNge -defZ rank_Ohm1 rankS // join_subG setSI // subsetI sZR. rewrite !(@rank_abelem _ p) // properG_ltn_log ?abelem_pgroup //= -/K properE. rewrite joing_subr join_subG subxx andbT subEproper; apply: contraL geH2. case/predU1P=> [defH | ltHZ]; last by rewrite -ltnNge -dimZ2 properG_ltn_log. rewrite -defH [H](setIidPl _) ?dimA3 // in dimZ2. by rewrite centsC -defH subIset // -abelianE cAA. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)