proposition: Theorem ps_poly_lap_summ : ∀ f g l, (∀ i, (f i = POL (g i))%pspol) → (ps_pol_summ ps_field l f = POL (ps_lap_summ ps_field l g))%pspol.
proof: Proof. intros f g l Hi. unfold ps_pol_eq, ps_pol in Hi. unfold ps_pol_eq, ps_pol, ps_pol_summ, ps_lap_summ. induction l as [| x]; [ reflexivity | simpl ]. rewrite <- eq_poly_lap_add. rewrite <- IHl, <- Hi. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m