proposition: Lemma interpolateE (p : {poly {poly R}}) : size p <= d -> interpolate (\row_i p.[points`_i]) = p.
proof: Proof. rewrite /interpolate => hsp; rewrite -[RHS](poly_rV_K hsp); congr rVpoly. apply/(canLR (mulmxK hU))/rowP=> i; rewrite !mxE (horner_coef_wide _ hsp). by apply: eq_bigr=> j _ ; rewrite !mxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div fintype tuple) mathcomp(finfun bigop fingroup perm ssralg zmodp matrix mxalgebra) mathcomp(poly polydiv mxpoly)