proposition: Theorem h_not_k : ∀ 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 ≠ k.
proof: Proof. intros pts j αj k αk seg. intros Hpts Hnp h αh Hαh Hnαh Hhk. eapply sorted_qeq_eq with (k := k) (αk := αk) in Hαh. rewrite Hαh in Hnαh; simpl in Hnαh. apply Decidable.not_or in Hnαh. destruct Hnαh as (_, Hnαh). apply Decidable.not_or in Hnαh. destruct Hnαh as (Hnαh, _). negation Hnαh. assumption. eapply in_ch_in_pts; eassumption. subst h; reflexivity. Qed.
imports: Utf8 QArith Sorting NPeano Misc Slope_base SlopeMisc ConvexHull ConvexHullMisc Newton NotInSegMisc