proposition: Lemma rVexp_neq0 i (a0 : a != 0) : rVexp ``_ i != 0.
proof: Proof. by rewrite mxE expf_eq0 /= negb_and a0 orbT. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv zmodp) mathcomp(matrix mxalgebra mxpoly vector cyclic perm) ssr_ext ssralg_ext hamming