proposition: Lemma poly_rV_K p : size p <= d -> rVpoly (poly_rV p) = p.
proof: Proof. move=> le_p_d; apply/polyP=> k; rewrite coef_rVpoly. case: insubP => [i _ <- | ]; first by rewrite mxE. by rewrite -ltnNge => le_d_l; rewrite nth_default ?(leq_trans le_p_d). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(div fintype tuple finfun bigop fingroup perm) mathcomp(ssralg zmodp matrix mxalgebra poly polydiv)