proposition: Theorem poly_summation_mul : ∀ l x g₁ g₂, (ps_pol_summ ps_field l (λ h, POL [(g₁ h * x)%ps] * g₂ h) = POL [x] * ps_pol_summ ps_field l (λ h, POL [g₁ h] * g₂ h))%pspol.
proof: Proof. intros l x g₁ g₂. progress unfold ps_pol_eq, eq_poly; simpl. progress unfold ps_pol_summ, lap_summation; simpl. induction l as [| i]; intros; simpl. rewrite lap_mul_nil_r; reflexivity. rewrite IHl. rewrite lap_mul_add_distr_l. simpl. apply lap_add_compat; [ reflexivity | simpl ]. rewrite lap_mul_assoc. apply lap_mul_compat; [ idtac | reflexivity ]. progress unfold lap_mul; simpl. rewrite summation_only_one; simpl. rewrite rng_mul_comm; 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