proposition: Theorem odd_p_abelian_constrained p G : odd #|G| -> solvable G -> p.-abelian_constrained G.
proof: Proof. move/odd_p_stable=> stabG /solvable_p_constrained constrG. exact: p_stable_abelian_constrained. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div fintype finset) mathcomp(prime fingroup morphism automorphism quotient gproduct gfunctor) mathcomp(cyclic center commutator pgroup nilpotent sylow abelian hall) mathcomp(maximal) odd_order(BGsection1 BGappendixAB)