proposition: Lemma sub_in_constt pi1 pi2 x : {in \pi(#[x]), {subset pi1 <= pi2}} -> x.`_pi2.`_pi1 = x.`_pi1.
proof: Proof. move=> pi12; rewrite -{2}(consttC pi2 x) consttM; last exact: commuteX2. rewrite (constt1P _ x.`_pi2^' _) ?mulg1 //. apply: sub_in_pnat (p_elt_constt _ x) => p; rewrite order_constt => pi_p. by apply/contra/pi12; rewrite -[#[x]](partnC pi2^') // primesM // pi_p. 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)