proposition: Lemma primitive_is_principal : n.-primitive_root a -> forall k, 1 <= k < n -> \sum_(j < n) a ^+ (j * k) = 0.
proof: Proof. move=> an k kn. move/(congr1 (fun x => x ^+ k)) : (prim_expr_order an). rewrite expr1n -exprM mulnC exprM => /eqP. rewrite -subr_eq0 => /eqP an1. suff : a ^+ k ^+ n - 1 = (a ^+ k - 1) * \sum_(j < n) a ^+ k ^+ j. rewrite an1 => /esym/eqP. rewrite mulf_eq0 => /orP[|/eqP tmp]. rewrite subr_eq0 -(prim_order_dvd an) gtnNdvd //; by case/andP : kn. rewrite -[in RHS]tmp. apply eq_bigr => i _; by rewrite mulnC exprM. rewrite mulrDl mulN1r. destruct n as [|n'] => //. rewrite {1}big_ord_recr /= mulrDr (addrC (a ^+ k * _)). rewrite -(exprM _ k n') -exprD -mulnS -exprM -addrA; congr (_ + _). rewrite big_distrr /= addrC big_ord_recl expr0 opprD. apply/eqP; rewrite -subr_eq; apply/eqP; congr (-1 - _). apply eq_bigr => i _. by rewrite -!exprM -exprD -mulnS. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming