proposition: Theorem hq_lt_kq : ∀ (f : puis_ser_pol α) hq αh kq αk L, newton_segments f = Some L → (hq, αh) ∈ oth_pts L → (kq, αk) = fin_pt L → hq < kq.
proof: Proof. intros f hq αh kq αk L HL Hoth Hfin. unfold newton_segments in HL. remember (points_of_ps_polynom f) as pts. apply points_of_polyn_sorted in Heqpts. unfold lower_convex_hull_points in HL. destruct pts as [| pt₁]; [ discriminate HL | idtac ]. destruct pts as [| pt₂]; [ discriminate HL | idtac ]. injection HL; clear HL; intros HL; subst L. simpl in Hoth, Hfin. eapply seg_bef_end_pt; try eassumption; 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