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