proposition: Lemma poly_rV_0_inv n (p : {poly R}) : size p <= n -> poly_rV p == (0 : 'rV[R]_n) -> p == 0.
proof: Proof. move=> pn /eqP p0; apply/eqP/polyP => i. case/boolP : (i < size p) => ip. - transitivity (poly_rV p 0 (widen_ord pn (Ordinal ip))); first by rewrite !mxE. by rewrite p0 mxE coef0. - by rewrite -(@poly_rV_K _ n p) // p0 linear0. Qed.
imports: mathcomp(all_ssreflect fingroup perm ssralg zmodp) mathcomp(matrix mxalgebra poly polydiv mxpoly) ssralg_ext