proposition: Lemma Ohm1_odd_ucn2 (Z := 'Ohm_1('Z_2(R))) : ~~ cyclic Z /\ exponent Z %| p.
proof: Proof. have [S nsSR Ep2S] := ex_odd_normal_p2Elem; have p_pr := pnElem_prime Ep2S. have [sSR abelS dimS] := pnElemP Ep2S; have [pS cSS expSp]:= and3P abelS. pose SR := [~: S, R]; pose SRR := [~: SR, R]. have nilR := pgroup_nil pR. have ntS: S :!=: 1 by rewrite -rank_gt0 (rank_abelem abelS) dimS. have sSR_S: SR \subset S by rewrite commg_subl normal_norm. have sSRR_SR: SRR \subset SR by rewrite commSg. have sSR_R := subset_trans sSR_S sSR. have{ntS} prSR: SR \proper S. by rewrite (nil_comm_properl nilR) // subsetI subxx -commg_subl. have SRR1: SRR = 1. have [SR1 | ntSR] := eqVneq SR 1; first by rewrite /SRR SR1 comm1G. have prSRR: SRR \proper SR. rewrite /proper sSRR_SR; apply: contra ntSR => sSR_SRR. by rewrite (forall_inP nilR) // subsetI sSR_R. have pSR := pgroupS sSR_R pR; have pSRR := pgroupS sSRR_SR pSR. have [_ _ [e oSR]] := pgroup_pdiv pSR ntSR; have [f oSRR] := p_natP pSRR. have e0: e = 0. have:= proper_card prSR; rewrite oSR (card_pnElem Ep2S). by rewrite ltn_exp2l ?prime_gt1 // !ltnS leqn0; move/eqP. apply/eqP; have:= proper_card prSRR; rewrite trivg_card1 oSR oSRR e0. by rewrite ltn_exp2l ?prime_gt1 // ltnS; case f. have sSR_ZR: [~: S, R] \subset 'Z(R). by rewrite subsetI sSR_R /=; apply/commG1P. have sS_Z2R: S \subset 'Z_2(R). rewrite ucnSnR; apply/subsetP=> s Ss; rewrite inE (subsetP sSR) //= ucn1. by rewrite (subset_trans _ sSR_ZR) ?commSg ?sub1set. have sZ2R_R := ucn_sub 2 R; have pZ2R := pgroupS sZ2R_R pR. have pZ: p.-group Z by apply: pgroupS pR; apply/gFsub_trans/gFsub. have sSZ: S \subset Z. by rewrite /Z (OhmE 1 pZ2R) sub_gen // subsetI sS_Z2R sub_LdivT. have ncycX: ~~ cyclic S by rewrite (abelem_cyclic abelS) dimS. split; first by apply: contra ncycX; apply: cyclicS. have nclZ2R : nil_class 'Z_2(R) <= 2 + _ := leq_trans (nil_class_ucn _ _) _. by have [] := exponent_odd_nil23 pZ2R (oddSg sZ2R_R oddR) (nclZ2R _ _). 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)