proposition: Theorem ps_monom_summation_aux : ∀ f b len, (ps_monom (summation_aux R b len f) 0 = summation_aux (ps_ring K) b len (λ i, ps_monom (f i) 0))%ps.
proof: Proof. intros f b len. revert b. induction len; intros; [ apply ps_zero_monom_eq | simpl ]. rewrite ps_monom_add_l. apply ps_add_compat_l. apply IHlen. 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