proposition: Lemma lagrange_poly_unique {R: fieldType} (pts: seq (R * R)) (q: {poly R}): uniq (unzip1 pts) -> (size q <= size pts)%N -> (forall x y, (x, y) \in pts -> q.[x] = y) -> q = lagrange_poly pts.
proof: Proof. move=> Huniq Hsize1 Hpred. assert (size (q - lagrange_poly pts)%R <= size pts)%N as Hsize. 1: { move: (size_lagrange_poly pts) => Hsize2. apply: leq_trans. 1: apply: size_add. by rewrite geq_max size_opp Hsize1 Hsize2. } apply /eqP. rewrite -GRing.subr_eq0 -size_poly_eq0. rewrite size_poly_eq0. apply /negPn /negP => Hcontra. rewrite leqNgt in Hsize. move /negP in Hsize. apply: Hsize. replace (size pts) with (size (unzip1 (pts))). 2: by rewrite size_map. apply: max_poly_roots => //. apply /allP => x' /mapP [[x y] Hin Heq]. subst. rewrite /root hornerD hornerN. rewrite (Hpred x y) //. rewrite (lagrange_poly_correct x y) //. by rewrite GRing.subr_eq0 eq_refl. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Mon(SPropBase) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb pkg_core_definition choice_type pkg_composition pkg_rhl Package Prelude) extructures(ord fset fmap) Equations(Equations)