proposition: Lemma lagrange_sub_zero_cons {R: fieldType} (x y1 y2: R) (pts: seq (R * R)): uniq (x :: unzip1 pts) -> lagrange_poly ((x, y1) :: pts) - lagrange_poly ((x, y2) :: pts) = lagrange_poly ((x, y1 - y2) :: zero_points (unzip1 pts)).
proof: Proof. move=> Huniq. apply: lagrange_poly_unique. - by rewrite /unzip1 map_cons -/unzip1 unzip1_zero_points. - apply: leq_trans. 1: by apply: size_add. rewrite size_opp /= !size_map geq_max. apply /andP. split. all: apply: leq_trans. 1,3: by apply: size_lagrange_poly. all: by []. - move=> x0 y0 Hin. rewrite in_cons in Hin. destruct (_ == _) eqn:Heq. + move /eqP in Heq. case: Heq => ? ?. subst. rewrite hornerD hornerN (lagrange_poly_correct x y1) //. 1: rewrite (lagrange_poly_correct x y2) //. all: by rewrite in_cons eq_refl. + rewrite (y_in_zero_points Hin). rewrite -!(cat1s _ pts). apply: lagrange_sub_zero => //. by apply: (x_in_zero_points x0 y0). 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)