proposition: Theorem h_not_j : ∀ pts j αj k αk seg, Sorted fst_lt pts → lower_convex_hull_points pts = Some (mkns (j, αj) (k, αk) seg) → ∀ h αh, (h, αh) ∈ pts → (h, αh) ∉ [(j, αj); (k, αk) … seg] → h ≠ j.
proof: Proof. intros pts j αj k αk seg. intros Hpts Hnp h αh Hαh Hnαh Hne. eapply sorted_qeq_eq with (k := j) (αk := αj) in Hαh; try eassumption. rewrite Hαh in Hnαh. simpl in Hnαh. apply Decidable.not_or in Hnαh. destruct Hnαh as (Hnαh, _). negation Hnαh. eapply in_ch_in_pts with (pt₂ := (k, αk)); eassumption. subst h; reflexivity. Qed.
imports: Utf8 QArith Sorting NPeano Misc Slope_base SlopeMisc ConvexHull ConvexHullMisc Newton NotInSegMisc