proposition: Lemma im_Zpm : Zpm @* Zp #[a] = <[a]>.
proof: Proof. apply/eqP; rewrite eq_sym eqEcard cycle_subG /= andbC morphimEdom. rewrite (leq_trans (leq_imset_card _ _)) ?card_Zp //= /Zp order_gt1. case: eqP => /= [a1 | _]; first by rewrite imset_set1 morph1 a1 set11. by apply/imsetP; exists 1%R; rewrite ?expg1 ?inE. 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)