proposition: Theorem ini_fin_ns_in_init_pts : ∀ pts L, lower_convex_hull_points pts = Some L → ini_pt L ∈ pts ∧ fin_pt L ∈ pts.
proof: Proof. intros pts L HL. eapply hull_seg_vert_in_init_pts; 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