proposition: Lemma lagrange_add_zero_cons {R: fieldType} (x y1 y2: R) (s: seq R): uniq (x :: s) -> lagrange_poly ((x, y1) :: zero_points s) + lagrange_poly ((x, y2) :: zero_points s) = lagrange_poly ((x, y1 + y2) :: zero_points s).
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_map geq_max. apply /andP. split. all: apply: leq_trans. 1,3: by apply: size_lagrange_poly. all: by rewrite /= size_map. - move=> x0 y0 Hin. rewrite in_cons in Hin. destruct (_ == _) eqn:Heq. + move /eqP in Heq. case: Heq => ? ?. subst. rewrite hornerD (lagrange_poly_correct x y1) //. 1: rewrite (lagrange_poly_correct x y2) //. 2,4: by rewrite in_cons eq_refl. all: by rewrite /unzip1 map_cons -/unzip1 unzip1_zero_points. + rewrite (y_in_zero_points Hin). rewrite -!(cat1s _ (zero_points s)). apply: lagrange_add_zero. 3: by apply: (x_in_zero_points x0 y0). all: by rewrite /unzip1 map_cons -/unzip1 unzip1_zero_points. 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)