proposition: Theorem lap_mul_summation : ∀ α (Rx : ring (puiseux_series α)) (Kx : field Rx) la l f, (la * lap_summation l f = lap_summation l (λ i, la * f i))%lap.
proof: Proof. intros α Rx Kx la l f. induction l as [| j]; intros; simpl. rewrite lap_mul_nil_r; reflexivity. rewrite lap_mul_add_distr_l, IHl. 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