proposition: Theorem f₁_eq_x_min_β₁_summation_split : ∀ f β₁ γ₁ c₁ l₁ l₂, split_list (List.seq 0 (length (al f))) l₁ l₂ → (next_pol f β₁ γ₁ c₁ = POL [ps_monom 1%K (- β₁)] * ps_pol_summ ps_field l₁ (λ (h : nat) (āh:=ps_poly_nth h f), POL [(āh * ps_monom 1%K (Qnat h * γ₁))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ h) + POL [ps_monom 1%K (- β₁)] * ps_pol_summ ps_field l₂ (λ (l : nat) (āl:=ps_poly_nth l f), POL [(āl * ps_monom 1%K (Qnat l * γ₁))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ l))%pspol.
proof: Proof. intros f β₁ γ₁ c₁ l₁ l₂ Hss. progress unfold ps_pol_add, ps_pol_mul, ps_pol_summ. rewrite <- poly_mul_add_distr_l. rewrite split_summation; [ idtac | eassumption ]. apply f₁_eq_x_min_β₁_summation; 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