proposition: Lemma prim_root_not_uroot_on : n.-primitive_root a -> not_uroot_on a n.
proof: Proof. destruct n as [|n'] => //. move/forallP => H k /andP[k0 kn]. rewrite -unity_rootE. move: (H (Ordinal (leq_ltn_trans (leq_pred k) kn))) => /=. rewrite prednK // => /eqP ->. by move: kn; rewrite ltnNge; apply: contra => /eqP ->. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming