proposition: Lemma Sylow_superset Q : Q \subset G -> p.-group Q -> {P : {group gT} | p.-Sylow(G) P & Q \subset P}.
proof: Proof. move=> sQG pQ. have [|P] := @maxgroup_exists _ (p.-subgroup(G)) Q; first exact/andP. by rewrite max_pgroup_Sylow; exists P. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype prime bigop finset fingroup morphism) mathcomp(automorphism quotient action cyclic gproduct) mathcomp(gfunctor commutator pgroup center nilpotent)