proposition: Lemma sub_pgroup pi rho A : {subset pi <= rho} -> pi.-group A -> rho.-group A.
proof: Proof. by move=> pi_sub_rho; apply: sub_in_pnat (in1W pi_sub_rho). 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)