proposition: Theorem split_summation : ∀ g l l₁ l₂, split_list l l₁ l₂ → (poly_summation l₁ g + poly_summation l₂ g = poly_summation l g)%pol.
proof: Proof. intros g l l₁ l₂ Hss. progress unfold poly_summation; simpl. progress unfold eq_poly; simpl. revert l₁ l₂ Hss. induction l as [| n]; intros; simpl. inversion Hss; subst; reflexivity. inversion Hss; subst; simpl. rewrite lap_add_shuffle0. rewrite IHl; [ reflexivity | assumption ]. rewrite lap_add_assoc. rewrite IHl; [ reflexivity | assumption ]. 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