proposition: Theorem poly_summation_add : ∀ g h l, (poly_summation l g + poly_summation l h = poly_summation l (λ i, g i + h i))%pol.
proof: Proof. intros g h l. progress unfold poly_summation, eq_poly; simpl. induction l as [| i]; intros; [ reflexivity | simpl ]. do 2 rewrite lap_add_assoc. apply lap_add_compat; [ idtac | reflexivity ]. rewrite lap_add_shuffle0. apply lap_add_compat; [ assumption | reflexivity ]. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol