proposition: Theorem hull_seg_edge_in_init_pts : ∀ pts hs pt, lower_convex_hull_points pts = Some hs → pt ∈ oth_pts hs → pt ∈ pts.
proof: Proof. intros pts hs pt Hnp Hpt. destruct pts as [| pt₁]; [ discriminate Hnp | idtac ]. destruct pts as [| pt₂]; [ discriminate Hnp | idtac ]. injection Hnp; clear Hnp; intros Hnp. subst hs; simpl in Hpt. right; eapply in_seg_in_pts; 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