proposition: Lemma order_constt pi (x : gT) : #[x.`_pi] = #[x]`_pi.
proof: Proof. rewrite -{2}(consttC pi x) orderM; [|exact: commuteX2|]; last first. by apply: (@pnat_coprime pi); apply: p_elt_constt. by rewrite partnM // part_pnat_id ?part_p'nat ?muln1 //; apply: p_elt_constt. 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)