proposition: Lemma comm_sub_max_pgroup pi H M G : [max M | pi.-subgroup(G) M] -> pi.-group H -> H \subset G -> commute H M -> H \subset M.
proof: Proof. case/maxgroupP=> /andP[sMG piM] maxM piH sHG cHM. rewrite -(maxM (H <*> M)%G) /= comm_joingE ?(mulG_subl, mulG_subr) //. by rewrite /psubgroup pgroupM piM piH mul_subG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)