proposition: Theorem edge_pts_sorted : ∀ pts hs, Sorted fst_lt pts → lower_convex_hull_points pts = Some hs → Sorted fst_lt (oth_pts hs).
proof: Proof. intros pts hs Hsort Hhs. destruct pts as [| pt₁]; [ easy | idtac ]. destruct pts as [| pt₂]; [ easy | idtac ]. unfold lower_convex_hull_points in Hhs. injection Hhs; clear Hhs; intros Hhs; subst hs; simpl. eapply minimise_slope_seg_sorted; [ 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