proposition: Lemma lagrange_coords (p : {poly_n K}) i : coord lagrange i p = p.[x i].
proof: Proof. rewrite [p in RHS](coord_basis lagrange_full) ?memvf //. rewrite (@big_morph _ _ _ 0%R +%R) // horner_sum. rewrite (bigD1 i) // big1 => [|j /= /negPf ji] /=; by rewrite ?hornerE nth_lagrange lagrange_sample ?eqxx ?ji ?mulr1 ?mulr0. 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)