proposition: Theorem lt_aft_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 → k < h → αj + j * ((αj - αk) / (k - j)) < αh + h * ((αj - αk) / (k - j)).
proof: Proof. intros pts j αj k αk seg Hsort Hnp h αh Hαh Hkh. eapply points_after_k; try reflexivity; try eassumption. destruct pts as [| pt₁]; [ discriminate Hnp | idtac ]. destruct pts as [| pt₂]; [ discriminate Hnp | idtac ]. injection Hnp; clear Hnp; intros; subst. eapply beg_lt_end_pt in Hsort; [ idtac | reflexivity ]. rewrite H0, H1 in Hsort. assumption. Qed.
imports: Utf8 QArith Sorting NPeano Misc Slope_base SlopeMisc ConvexHull ConvexHullMisc Newton NotInSegMisc