proposition: Theorem subst_αh_hγ : ∀ f L pl tl l₁ c₁, 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 → (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 * γ L))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ h) = ps_pol_summ ps_field l₁ (λ h, let ah := ps_monom (coeff_of_term h tl) 0 in POL [(ah * ps_monom 1%K (β L))%ps] * POL [ps_monom c₁ 0; 1%ps … []] ^ h))%pspol.
proof: Proof. intros f L pl tl l₁ c₁ HL Hpl Htl Hl. progress unfold eq_poly; simpl. apply lap_eq_list_fold_right. intros h a b Hh Heq. apply lap_add_compat; [ assumption | simpl ]. apply lap_mul_compat; [ simpl | reflexivity ]. constructor; [ idtac | reflexivity ]. apply rng_mul_compat; [ reflexivity | simpl ]. rewrite points_in_any_newton_segment; [ reflexivity | eassumption | idtac ]. apply list_in_cons_app. remember HL as Hsort; clear HeqHsort. apply ini_oth_fin_pts_sorted in Hsort. rewrite <- Hpl in Hsort; rewrite <- Hpl. subst tl l₁. rewrite List.map_map in Hh; simpl in Hh. assert (∀ pt, pt ∈ pl → ∃ h αh, pt = (Qnat h, αh)) as Hnat. intros pt Hpt. eapply points_in_newton_segment_have_nat_abscissa; [ eassumption | idtac ]. subst pl; assumption. apply ord_is_ord_of_pt; 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