proposition: Lemma eq_prim_root_expr i j : (z ^+ i == z ^+ j) = (i == j %[mod n]).
proof: Proof. wlog le_ji: i j / j <= i. move=> IH; case: (leqP j i) => [|/ltnW] /IH //. by rewrite eq_sym (eq_sym (j %% n)%N). rewrite -{1}(subnKC le_ji) exprD -prim_expr_mod eqn_mod_dvd //. rewrite prim_order_dvd; apply/eqP/eqP=> [|->]; last by rewrite mulr1. move/(congr1 ( *%R (z ^+ (n - j %% n)))); rewrite mulrA -exprD. by rewrite subnK ?prim_expr_order ?mul1r // ltnW ?ltn_mod. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)