proposition: Lemma Ohm1_metacyclic_p2Elem gT p (R : {group gT}) : metacyclic R -> p.-group R -> odd #|R| -> ~~ cyclic R -> 'Ohm_1(R)%G \in 'E_p^2(R).
proof: Proof. case/metacyclicP=> S [cycS nsSR cycRb] pR oddR ncycR. have [[sSR nSR] [s defS]] := (andP nsSR, cyclicP cycS). have [T defTb sST sTR] := inv_quotientS nsSR (Ohm_sub 1 (R / S)). have [pT oddT] := (pgroupS sTR pR, oddSg sTR oddR). have Ts: s \in T by rewrite -cycle_subG -defS. have iTs: #|T : <[s]>| = p. rewrite -defS -card_quotient ?(subset_trans sTR) // -defTb. rewrite (Ohm1_cyclic_pgroup_prime cycRb (quotient_pgroup _ pR)) // -subG1. by rewrite quotient_sub1 ?(contra (fun sRS => cyclicS sRS cycS)). have defR1: 'Ohm_1(R) = 'Ohm_1(T). apply/eqP; rewrite eqEsubset (OhmS _ sTR) andbT -Ohm_id OhmS //. by rewrite -(quotientSGK _ sST) ?gFsub_trans // -defTb morphim_Ohm. rewrite (subsetP (pnElemS _ _ sTR)) // (group_inj defR1). apply: Ohm1_extremal_odd iTs => //; apply: contra ncycR. by rewrite !(@odd_pgroup_rank1_cyclic _ p) // -p_rank_Ohm1 -defR1 p_rank_Ohm1. 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)