proposition: Lemma rVexp_inj (a0 : a != 0) (H : not_uroot_on a n) : injective [ffun i => rVexp ``_ i].
proof: Proof. move=> i j. rewrite 2!ffunE 2!mxE => /eqP. by rewrite exp_inj // => /eqP. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming