proposition: Theorem f₁_eq_sum_α_hγ_to_rest : ∀ f L β₁ γ₁ c₁ pl tl l₁ l₂, newton_segments f = Some L → pl = [ini_pt L … oth_pts L ++ [fin_pt L]] → tl = List.map (term_of_point f) pl → l₁ = List.map (λ t, power t) tl → 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, let ah := ps_monom (coeff_of_term h tl) 0 in let αh := ord_of_pt h pl in POL [(ah * ps_monom 1%K (αh + Qnat h * γ₁))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ h) + POL [ps_monom 1%K (- β₁)] * (ps_pol_summ ps_field l₁ (λ h, let āh := ps_poly_nth h f in let ah := ps_monom (coeff_of_term h tl) 0 in let αh := ord_of_pt h pl in POL [((āh - ah * ps_monom 1%K αh) * ps_monom 1%K (Qnat h * γ₁))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ h) + ps_pol_summ ps_field l₂ (λ l, let āl := ps_poly_nth l f in POL [(āl * ps_monom 1%K (Qnat l * γ₁))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ l)))%pspol.
proof: Proof. intros f L β₁ γ₁ c₁ pl tl l₁ l₂ HL Hpl Htl Hl Hss. progress unfold ps_pol_add at 2. progress unfold ps_pol_mul at 3. rewrite poly_mul_add_distr_l. progress unfold ps_pol_add at 1. rewrite poly_add_assoc. progress unfold ps_pol_mul at 1. rewrite <- poly_mul_add_distr_l. rewrite fold_ps_pol_add, fold_ps_pol_mul. rewrite fold_ps_pol_add, fold_ps_pol_mul. rewrite <- summation_split_val; try eassumption. apply f₁_eq_x_min_β₁_summation_split; 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