proposition: Theorem lt_bet_j_and_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] → j < h < k → αj + j * ((αj - αk) / (k - j)) < αh + h * ((αj - αk) / (k - j)).
proof: Proof. intros pts j αj k αk seg Hsort Hnp. intros h αh Hαh Hnαh Hjhk. 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). eapply points_between_j_and_k; try eassumption; reflexivity. Qed.
imports: Utf8 QArith Sorting NPeano Misc Slope_base SlopeMisc ConvexHull ConvexHullMisc Newton NotInSegMisc