proposition: Theorem points_between_j_and_k : ∀ pts j αj k αk oth γ β, Sorted fst_lt pts → γ = (αj - αk) / (k - j) → β = αj + j * γ → lower_convex_hull_points pts = Some (mkns (j, αj) (k, αk) oth) → ∀ h αh, j < h < k → (h, αh) ∈ pts → (h, αh) ∉ oth → β < αh + h * γ.
proof: Proof. intros pts j αj k αk oth γ β. intros Hsort Hγ Hβ Hnp h αh (Hjh, Hhk) Hαh Hseg. destruct pts as [| pt₁]; [ discriminate Hnp | idtac ]. remember Hnp as H; clear HeqH. apply next_ch_points_hd in H. subst pt₁; simpl in Hnp. destruct pts as [| pt₁]; [ discriminate Hnp | idtac ]. remember (minimise_slope (j, αj) pt₁ pts) as ms₁. injection Hnp; clear Hnp; intros Hop₁ Hep₁ Hbp₁; subst oth. destruct Hαh as [Hαh| Hαh]. injection Hαh; clear Hαh; intros; subst h αh. apply Qlt_irrefl in Hjh; contradiction. destruct Hαh as [Hαh| Hαh]. subst pt₁. symmetry in Heqms₁. destruct pts as [| pt₁]. simpl in Heqms₁. subst ms₁. simpl in Hep₁, Hseg, Hbp₁. injection Hep₁; clear Hep₁; intros; subst h αh. apply Qlt_irrefl in Hhk; contradiction. simpl in Heqms₁. remember (minimise_slope (j, αj) pt₁ pts) as ms₂. symmetry in Heqms₂. remember (slope_expr (j, αj) (h, αh) ?= slope ms₂) as c. destruct c; subst ms₁. simpl in Hep₁, Hseg, Hbp₁. apply Decidable.not_or in Hseg. destruct Hseg as (H, _); negation H. simpl in Hep₁, Hseg, Hbp₁. injection Hep₁; clear Hep₁; intros; subst h αh. apply Qlt_irrefl in Hhk; contradiction. symmetry in Hep₁. remember Heqms₂ as H; clear HeqH. eapply minimised_slope in H; [ idtac | eassumption ]. symmetry in Heqc; apply Qgt_alt in Heqc. rewrite H in Heqc. subst β γ. apply ad_hoc_lt_lt. split; [ assumption | idtac ]. eapply Qlt_trans; eassumption. unfold slope_expr in Heqc; simpl in Heqc. assumption. symmetry in Heqms₁. revert pt₁ ms₁ Hsort Heqms₁ Hep₁ Hseg Hbp₁. induction pts as [| pt₂]; intros. simpl in Heqms₁. subst ms₁. simpl in Hep₁, Hseg, Hbp₁. contradiction. destruct Hαh as [Hαh| Hαh]. subst pt₂. symmetry in Hep₁. remember Heqms₁ as H; clear HeqH. eapply minimised_slope in H; [ idtac | eassumption ]. symmetry in Hep₁. eapply not_seg_min_sl_lt in Heqms₁; try eassumption. rewrite H in Heqms₁. subst β γ. apply ad_hoc_lt_lt. split; [ assumption | idtac ]. eapply Qlt_trans; eassumption. unfold slope_expr in Heqms₁; simpl in Heqms₁. assumption. split; assumption. simpl in Heqms₁. remember (minimise_slope (j, αj) pt₂ pts) as ms₂. symmetry in Heqms₂. remember (slope_expr (j, αj) pt₁ ?= slope ms₂) as c. symmetry in Heqc. destruct c; subst ms₁. simpl in Hep₁, Hseg, Hbp₁. apply Decidable.not_or in Hseg. destruct Hseg as (Hlt₁, Hseg). eapply IHpts; try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. rewrite <- Heqms₂, minimised_slope_beg_pt; reflexivity. simpl in Hep₁, Hseg, Hbp₁. subst pt₁. apply Sorted_inv_2 in Hsort. destruct Hsort as (Hlt₂, Hsort). apply Sorted_inv_2 in Hsort. destruct Hsort as (Hlt₃, Hsort). eapply Sorted_hd in Hsort; [ idtac | eassumption ]. unfold fst_lt in Hlt₃. simpl in Hlt₃, Hsort. clear Hlt₂. eapply Qlt_trans in Hlt₃; [ idtac | eassumption ]. eapply Qlt_trans in Hlt₃; [ idtac | eassumption ]. apply Qlt_irrefl in Hlt₃; contradiction. eapply IHpts; try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. Qed.
imports: Utf8 QArith Sorting Misc Slope_base ConvexHull ConvexHullMisc