proposition: Lemma rVpoly_is_linear : linear rVpoly.
proof: Proof. move=> a u v; apply/polyP=> k; rewrite coefD coefZ !coef_rVpoly. by case: insubP => [i _ _ | _]; rewrite ?mxE // mulr0 addr0. 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)