proposition: Lemma aut_prim_rootP u z n : n.-primitive_root z -> {k | coprime k n & u z = z ^+ k}.
proof: Proof. move=> prim_z; have:= prim_z; rewrite -(fmorph_primitive_root u) => prim_uz. have [[k _] /= def_uz] := prim_rootP prim_z (prim_expr_order prim_uz). by exists k; rewrite // -(prim_root_exp_coprime _ prim_z) -def_uz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)