proposition: Proposition odd_normal_p2Elem_exists gT p (R S : {group gT}) : p.-group R -> odd #|R| -> S <| R -> ~~ cyclic S -> exists E : {group gT}, [/\ E \subset S, E <| R & E \in 'E_p^2(R)].
proof: Proof. move=> pR oddR nsSR ncycS; have sSR := normal_sub nsSR. have{sSR ncycS} []:= Ohm1_odd_ucn2 (pgroupS sSR pR) (oddSg sSR oddR) ncycS. set Z := 'Ohm_1(_) => ncycZ expZp. have chZS: Z \char S by rewrite !gFchar_trans. have{nsSR} nsZR: Z <| R := char_normal_trans chZS nsSR. have [sZR _] := andP nsZR; have pZ: p.-group Z := pgroupS sZR pR. have geZ2: 2 <= logn p #|Z|. rewrite (odd_pgroup_rank1_cyclic pZ (oddSg sZR oddR)) -ltnNge /= -/Z in ncycZ. by case/p_rank_geP: ncycZ => E; case/pnElemP=> sEZ _ <-; rewrite lognSg. have [E [sEZ nsER oE]] := normal_pgroup pR nsZR geZ2. have [sER _] := andP nsER; have{pR} pE := pgroupS sER pR. have{geZ2} p_pr: prime p by move: geZ2; rewrite lognE; case: (prime p). have{oE p_pr} dimE2: logn p #|E| = 2 by rewrite oE pfactorK. exists E; split; rewrite ?(subset_trans _ (char_sub chZS)) {chZS nsZR}//. rewrite !inE /abelem sER pE (p2group_abelian pE) dimE2 //= andbT. exact/(dvdn_trans _ expZp)/exponentS. 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)