proposition: Lemma lagrange_gen (p : {poly K}) : (size p <= n)%N -> p = \sum_(i < n) p.[x i]%:P * lagrange_ i.
proof: Proof. move=> sp; rewrite -[p](@npolypK _ n) //. rewrite [npolyp _ _ in LHS](coord_basis lagrange_full) ?memvf //. rewrite (@big_morph _ _ _ 0%R +%R) //; apply: eq_bigr=> i _. by rewrite lagrange_coords mul_polyC nth_lagrange. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun ssralg countalg finalg poly polydiv) mathcomp(perm fingroup matrix mxalgebra mxpoly vector countalg)