proposition: Lemma exp_prim_root k : (n %/ gcdn k n).-primitive_root (z ^+ k).
proof: Proof. set d := gcdn k n; have d_gt0: (0 < d)%N by rewrite gcdn_gt0 orbC n_gt0. have [d_dv_k d_dv_n]: (d %| k /\ d %| n)%N by rewrite dvdn_gcdl dvdn_gcdr. set q := (n %/ d)%N; rewrite /q.-primitive_root ltn_divRL // n_gt0. apply/forallP=> i; rewrite unity_rootE -exprM -prim_order_dvd. rewrite -(divnK d_dv_n) -/q -(divnK d_dv_k) mulnAC dvdn_pmul2r //. apply/eqP; apply/idP/idP=> [|/eqP->]; last by rewrite dvdn_mull. rewrite Gauss_dvdr; first by rewrite eqn_leq ltn_ord; apply: dvdn_leq. by rewrite /coprime gcdnC -(eqn_pmul2r d_gt0) mul1n muln_gcdl !divnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)