proposition: Lemma Zp_unitmM : {in units_Zp #[a] &, {morph Zp_unitm : u v / u * v}}.
proof: Proof. move=> u v _ _; apply: (eq_Aut (Aut_aut _ _)) => [|x a_x]. by rewrite groupM ?Aut_aut. rewrite permM !autE ?groupX //= /cyclem -expgM. rewrite -expg_mod_order modn_dvdm ?expg_mod_order //. case: (leqP #[a] 1) => [lea1 | lt1a]; last by rewrite Zp_cast ?order_dvdG. by rewrite card_le1_trivg // in a_x; rewrite (set1P a_x) order1 dvd1n. 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)