proposition: Lemma ZgroupS G H : H \subset G -> Zgroup G -> Zgroup H.
proof: Proof. move=> sHG /forallP zgG; apply/forall_inP=> V /SylowP[p p_pr /and3P[sVH]]. case/(Sylow_superset (subset_trans sVH sHG))=> P sylP sVP _. by have:= zgG P; rewrite (p_Sylow sylP); apply: cyclicS. 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)