proposition: Lemma injm_Zpm : 'injm Zpm.
proof: Proof. apply/injmP/dinjectiveP/card_uniqP. rewrite size_map -cardE card_Zp //= {7}/order -im_Zpm morphimEdom /=. by apply: eq_card => x; apply/imageP/imsetP=> [] [i Zp_i ->]; exists i. 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)