proposition: Lemma consttC pi x : x.`_pi * x.`_pi^' = x.
proof: Proof. apply/eqP; rewrite -{3}[x]expg1 -expgD eq_expg_mod_order. rewrite partnNK -{5 6}(@partnC pi #[x]) // /chinese !addn0. by rewrite chinese_remainder ?chinese_modl ?chinese_modr ?coprime_partC ?eqxx. 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)