proposition: Lemma sub_p_elt pi1 pi2 x : {subset pi1 <= pi2} -> pi1.-elt x -> pi2.-elt x.
proof: Proof. by move=> pi12; apply: sub_in_pnat => q _; apply: pi12. 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)