proposition: Lemma im_Zp_unitm : Zp_unitm @* units_Zp #[a] = Aut <[a]>.
proof: Proof. rewrite morphimEdom; apply/setP=> f; pose n := invm (injm_Zpm a) (f a). apply/imsetP/idP=> [[u _ ->] | Af]; first exact: Aut_aut. have [a1 | nta] := eqVneq a 1. by rewrite a1 cycle1 Aut1 in Af; exists 1; rewrite // morph1 (set1P Af). have a_fa: <[a]> = <[f a]>. by rewrite -(autmE Af) -morphim_cycle ?im_autm ?cycle_id. have def_n: a ^+ n = f a. by rewrite -/(Zpm n) invmK // im_Zpm a_fa cycle_id. have co_a_n: coprime #[a].-2.+2 n. by rewrite {1}Zp_cast ?order_gt1 // -generator_coprime def_n; apply/eqP. exists (FinRing.unit 'Z_#[a] co_a_n); rewrite ?inE //. apply: eq_Aut (Af) (Aut_aut _ _) _ => x ax. rewrite autE //= /cyclem; case/cycleP: ax => k ->{x}. by rewrite -(autmE Af) morphX ?cycle_id //= autmE -def_n -!expgM mulnC. 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)