proposition: Theorem lt_bef_j : ∀ pts j αj segjk k αk, Sorted fst_lt pts → lower_convex_hull_points pts = Some (mkns (j, αj) (k, αk) segjk) → ∀ h αh, (h, αh) ∈ pts → h < j < k → αj + j * ((αj - αk) / (k - j)) < αh + h * ((αj - αk) / (k - j)).
proof: Proof. intros pts j αj segjk k αk. intros Hsort Hnp h αh Hαh (Hhj, Hjk). destruct pts as [| pt₁]; [ discriminate Hnp | idtac ]. destruct pts as [| pt₂]; [ discriminate Hnp | idtac ]. simpl in Hnp. rewrite minimised_slope_beg_pt in Hnp. injection Hnp; clear Hnp; intros; subst pt₁. rename H into Hnp. rename H0 into Hseg. destruct Hαh as [Hαh| Hαh]. injection Hαh; clear Hαh; intros; subst h αh. apply Qlt_irrefl in Hhj; contradiction. eapply Sorted_hd in Hsort; [ idtac | eassumption ]. eapply Qlt_trans in Hhj; [ idtac | eassumption ]. apply Qlt_irrefl in Hhj; contradiction. Qed.
imports: Utf8 QArith Sorting NPeano Misc Slope_base SlopeMisc ConvexHull ConvexHullMisc Newton NotInSegMisc