proposition: Lemma narrow_structureP : reflect (narrow_structure p R) (p.-narrow R).
proof: Proof. apply: (iffP idP) => [nnR | [S C sSR sCR oS cycC defSC]]. have [S [sSR oS rCRS]] := narrow_centP nnR. have [cycC _ _ defCRS] := narrow_cent_dprod nnR oS sSR rCRS. by exists S [group of 'C_T(S)]; rewrite //= -setIA subsetIl. apply/narrow_centP; exists S; split=> //. have cycS: cyclic S by rewrite prime_cyclic ?oS. rewrite -(p_rank_dprod p defSC) -!(rank_pgroup (pgroupS _ pR)) // -addn1. rewrite leq_add -?abelian_rank1_cyclic ?cyclic_abelian //. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finset prime fingroup morphism perm automorphism action) mathcomp(quotient cyclic gfunctor pgroup gproduct center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection4)