proposition: Lemma primitive_uroot_neq0 : n.+1.-primitive_root a -> a != 0.
proof: Proof. move=> abs; apply/negP => /eqP ?; subst a. move/prim_expr_order : abs. by rewrite expr0n /= => /eqP; rewrite eq_sym oner_eq0. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming