proposition: Lemma not_uroot_on_prim_root : not_uroot_on a n.+1 -> a ^+ n.+1 = 1 -> n.+1.-primitive_root a.
proof: Proof. move=> H an1. apply/forallP => /= i. rewrite unity_rootE -an1. case/boolP : (a == 0) => [/eqP ?|a0]. subst a. move: an1; rewrite expr0n /= => /eqP. by rewrite eq_sym oner_eq0. rewrite !exprS. apply/eqP; apply/idP/idP => /eqP. move: (exp_inj a0 H i (Ordinal (ltnSn n))) => H' /mulrI. rewrite unitfE => /(_ a0) /eqP. by rewrite H' => /eqP ->. by case=> ->. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming