proposition: Theorem qeq_eq_fin : ∀ pts h αh k αk ptk s, Sorted fst_lt pts → lower_convex_hull_points pts = Some (mkns ptk (k, αk) s) → (h, αh) ∈ pts → h == k → h = k.
proof: Proof. intros pts h αh k αk ptk s Hpts Hhsl Hαh Hhk. eapply sorted_qeq_eq with (αk := αk) in Hhk; try eassumption. injection Hhk; intros; subst; reflexivity. now apply in_ch_in_pts with (s := s) (pt₁ := ptk). Qed.
imports: Utf8 QArith Sorting Misc Slope_base ConvexHull ConvexHullMisc