proposition: Theorem ini_oth_fin_pts_sorted : ∀ f L, newton_segments f = Some L → Sorted fst_lt [ini_pt L … oth_pts L ++ [fin_pt L]].
proof: Proof. intros f L HL. constructor. remember HL as HL_v; clear HeqHL_v. unfold newton_segments in HL. remember (points_of_ps_polynom f) as pts. apply points_of_polyn_sorted in Heqpts. apply Sorted_app_at_r. eapply edge_pts_sorted; eassumption. intros (hq, αh) Hh. eapply hq_lt_kq; try eassumption. symmetry; apply surjective_pairing. remember HL as Hini; clear HeqHini. apply exists_ini_pt_nat in Hini. destruct Hini as (j, (aj, Hini)). remember HL as Hfin; clear HeqHfin. apply exists_fin_pt_nat in Hfin. destruct Hfin as (k, (ak, Hfin)). symmetry in Hini, Hfin. apply HdRel_app. remember (oth_pts L) as pts eqn:Hpts . symmetry in Hpts. destruct pts as [| (h, ah)]; constructor. rewrite <- Hini; unfold fst_lt; simpl. eapply jq_lt_hq; try eassumption. rewrite Hpts; left; reflexivity. constructor. rewrite <- Hini, <- Hfin; unfold fst_lt; simpl. unfold Qlt; simpl. do 2 rewrite Z.mul_1_r. eapply jz_lt_kz; try eassumption. rewrite <- Hini; reflexivity. rewrite <- Hfin; reflexivity. Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base