proposition: Lemma prim_root_exp_coprime n z k : n.-primitive_root z -> n.-primitive_root (z ^+ k) = coprime k n.
proof: Proof. move=> prim_z; have n_gt0 := prim_order_gt0 prim_z. apply/idP/idP=> [prim_zk | co_k_n]. set d := gcdn k n; have dv_d_n: (d %| n)%N := dvdn_gcdr _ _. rewrite /coprime -/d -(eqn_pmul2r n_gt0) mul1n -{2}(gcdnMl n d). rewrite -{2}(divnK dv_d_n) (mulnC _ d) -muln_gcdr (gcdn_idPr _) //. rewrite (prim_order_dvd prim_zk) -exprM -(prim_order_dvd prim_z). by rewrite muln_divCA_gcd dvdn_mulr. have zkn_1: z ^+ k ^+ n = 1 by rewrite exprAC (prim_expr_order prim_z) expr1n. have{zkn_1} [m prim_zk dv_m_n]:= prim_order_exists n_gt0 zkn_1. suffices /eqP <-: m == n by []. rewrite eqn_dvd dv_m_n -(@Gauss_dvdr n k m) 1?coprime_sym //=. by rewrite (prim_order_dvd prim_z) exprM (prim_expr_order prim_zk). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)