proposition: Lemma ZpmM : {in Zp #[a] &, {morph Zpm : x y / x * y}}.
proof: Proof. rewrite /Zpm; case: (eqVneq a 1) => [-> | nta] i j _ _. by rewrite !expg1n ?mulg1. by rewrite /= {3}Zp_cast ?order_gt1 // expg_mod_order expgD. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)