proposition: Lemma injm_Zp_unitm : 'injm Zp_unitm.
proof: Proof. have [a1 | nta] := eqVneq a 1. by rewrite subIset //= card_le1_trivg ?subxx // card_units_Zp a1 order1. apply/subsetP=> /= u /morphpreP[_ /set1P/= um1]. have{um1}: Zp_unitm u a == Zp_unitm 1 a by rewrite um1 morph1. rewrite !autE ?cycle_id // eq_expg_mod_order. by rewrite -[n in _ == _ %[mod n]]Zp_cast ?order_gt1 // !modZp 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)