proposition: Theorem f₁_eq_sum_without_x_β₁_plus_sum : ∀ 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 (β L) (γ L) c₁ = ps_pol_summ ps_field l₁ (λ h, let ah := ps_monom (coeff_of_term h tl) 0 in POL [ah] * POL [ps_monom c₁ 0; 1%ps … []] ^ h) + POL [ps_monom 1%K (- β L)] * (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 * γ L))%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 * γ 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. remember HL as H; clear HeqH. eapply f₁_eq_sum_α_hγ_to_rest in H; try eassumption. rewrite H. apply poly_add_compat; [ idtac | reflexivity ]. rewrite subst_αh_hγ; try eassumption; simpl. rewrite poly_summation_mul. progress unfold ps_pol_mul. rewrite poly_mul_assoc. symmetry. rewrite <- poly_mul_1_l in |- * at 1. apply poly_mul_compat; [ idtac | reflexivity ]. progress unfold poly_mul; simpl. progress unfold eq_poly; simpl. progress unfold ps_one; simpl. progress unfold lap_mul; simpl. rewrite summation_only_one; simpl. constructor; [ idtac | reflexivity ]. progress unfold ps_monom; simpl. progress unfold ps_mul; simpl. progress unfold cm; simpl. rewrite Z.mul_opp_l. rewrite Z.add_opp_diag_l. rewrite stretch_series_1, series_mul_1_l. remember (Qden (β L) * Qden (β L))%positive as k. rewrite ps_adjust_eq with (k := k) (n := O). progress unfold adjust_ps; simpl. rewrite series_shift_0, stretch_series_1. subst k; 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