proposition: Theorem rank2_sub_p'core_der1 gT (G A : {group gT}) p : solvable G -> odd #|G| -> 'r_p(G) <= 2 -> p^'.-subgroup(G^`(1)) A -> A \subset 'O_p^'(G^`(1)).
proof: Proof. move=> solG oddG rG /andP[sAG' p'A]; rewrite sub_Hall_pcore //. by have [-> _ _] := rank2_der1_complement solG oddG rG. 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)