proposition: Theorem points_after_k : ∀ pts j αj k αk seg γ β, Sorted fst_lt pts → j < k → γ = (αj - αk) / (k - j) → β = αj + j * γ → lower_convex_hull_points pts = Some (mkns (j, αj) (k, αk) seg) → ∀ h αh, k < h → (h, αh) ∈ pts → β < αh + h * γ.
proof: Proof. intros pts j αj k αk seg γ β. intros Hsort Hjk Hγ Hβ Hnp h αh Hkh Hαh. destruct pts as [| pt₁]; [ easy | ]. destruct pts as [| pt₂]; [ easy | ]. simpl in Hnp. rewrite minimised_slope_beg_pt in Hnp. injection Hnp; clear Hnp; intros Hseg Hep₁ Hp₁; subst seg pt₁. remember (minimise_slope (j, αj) pt₂ pts) as ms₁. destruct Hαh as [Hαh| Hαh]. injection Hαh; clear Hαh; intros; subst h αh. eapply Qlt_trans in Hkh; [ idtac | eassumption ]. apply Qlt_irrefl in Hkh; contradiction. destruct Hαh as [Hαh| Hαh]; [ exfalso | idtac ]. subst pt₂. symmetry in Heqms₁. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt₁, Hsort). apply minimise_slope_le in Heqms₁; [ idtac | assumption ]. rewrite Hep₁ in Heqms₁. apply Qle_not_lt in Heqms₁. contradiction. symmetry in Heqms₁. symmetry in Hep₁. remember Heqms₁ as H; clear HeqH. eapply minimised_slope in H; [ idtac | eassumption ]. symmetry in Hep₁. eapply min_slope_lt_after_k in Heqms₁; try eassumption. rewrite H in Heqms₁. subst β γ. apply ad_hoc_lt_lt. split; [ idtac | assumption ]. eapply Qlt_trans; eassumption. unfold slope_expr in Heqms₁; simpl in Heqms₁. assumption. apply Sorted_inv_2 in Hsort; destruct Hsort as (Hlt, Hsort). apply Sorted_inv_1 in Hsort; assumption. Qed.
imports: Utf8 QArith Sorting Misc Slope_base ConvexHull ConvexHullMisc