proposition: Theorem vert_bef_edge : ∀ pts hs j αj h αh, Sorted fst_lt pts → lower_convex_hull_points pts = Some hs → (j, αj) = ini_pt hs → (h, αh) ∈ oth_pts hs → j < h.
proof: Proof. intros pts hs j αj h αh Hsort Hnp Hj Hh. destruct pts as [| pt₁]; [ discriminate Hnp | idtac ]. destruct pts as [| pt₂]; [ discriminate Hnp | idtac ]. injection Hnp; clear Hnp; intros Hhsl; subst hs. simpl in Hj, Hh. rewrite minimised_slope_beg_pt in Hj. apply pt₁_bef_seg in Hh; [ subst pt₁; assumption | assumption ]. 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