proposition: Lemma lagrange_free : free lagrange.
proof: Proof. apply/freeP=> lambda eq_l i. have /(congr1 (fun p : {poly__ _} => p.[x i])) := eq_l. rewrite (@big_morph _ _ _ 0%R +%R) // horner_sum horner0. 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)