proposition: Theorem ps_lap_in_summation : ∀ f l, (∀ i, i ∈ l → ∀ m, ps_lap_in m (f i) → (order m > 0)%Qbar) → (∀ m, ps_lap_in m (ps_lap_summ ps_field l f) → (order m > 0)%Qbar).
proof: Proof. intros f l Hi m Hm. revert m Hm. induction l as [| j]; intros; [ contradiction | idtac ]. simpl in Hm. apply ps_lap_in_add in Hm; [ assumption | idtac | idtac ]. intros n Hn. apply IHl; [ idtac | assumption ]. intros k Hk p Hp. eapply Hi; [ idtac | eassumption ]. right; assumption. intros k Hk. eapply Hi; [ idtac | eassumption ]. left; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted Misc NbarM QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHull ConvexHullMisc PolyConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq