proposition: Lemma narrowJ x : p.-narrow (R :^ x) = p.-narrow R.
proof: Proof. by apply: isog_narrow (isog_symr (conj_isog R x)). 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)