proposition: Theorem oth_pts_in_init_pts : ∀ pts L pt, lower_convex_hull_points pts = Some L → pt ∈ oth_pts L → pt ∈ pts.
proof: Proof. intros pts L pt HL Hpt. eapply hull_seg_edge_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