proposition: Theorem jq_lt_hq : ∀ (f : puis_ser_pol α) j αj h αh L, newton_segments f = Some L → (j, αj) = ini_pt L → (h, αh) ∈ oth_pts L → j < h.
proof: Proof. intros f j αj h αh L HL Hjαj Hhαh. unfold newton_segments in HL. remember (points_of_ps_polynom f) as pts. apply points_of_polyn_sorted in Heqpts. eapply vert_bef_edge; eassumption. 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