proposition: Lemma distinct_non_zero_rVexp (a : F) (a0 : a != 0) (H : not_uroot_on a n) : distinct_non_zero (rVexp a n).
proof: Proof. rewrite /distinct_non_zero; split; first by apply rVexp_inj. move=> ?; by rewrite mxE expf_neq0. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly) ssr_ext ssralg_ext cyclic_code dft