proposition: Theorem not_seg_min_sl_lt : ∀ j αj k αk pt pts ms h αh, Sorted fst_lt [(j, αj); pt; (h, αh) … pts] → minimise_slope (j, αj) pt [(h, αh) … pts] = ms → j < h < k → (h, αh) ∉ oth_pts ms → fin_pt ms = (k, αk) → slope ms < slope_expr (j, αj) (h, αh).
proof: Proof. intros j αj k αk pt pts ms h αh Hsort Hms (Hjh, Hhk) Hseg Hep. rewrite slope_slope_expr; [ idtac | eassumption ]. revert ms Hms Hseg Hep. induction pts as [| pt₁]; intros. simpl in Hms. unfold slope in Hms; simpl in Hms. remember (slope_expr (j, αj) pt ?= slope_expr (j, αj) (h, αh)) as c. symmetry in Heqc. destruct c; subst ms; simpl. simpl in Hseg, Hep. injection Hep; clear Hep; intros; subst h αh. apply Qlt_irrefl in Hhk; contradiction. simpl in Hseg, Hep. subst pt. apply Qlt_alt in Heqc. assumption. simpl in Hseg, Hep. injection Hep; clear Hep; intros; subst h αh. apply Qlt_irrefl in Hhk; contradiction. remember [pt₁ … pts] as pts₁. simpl in Hms. remember (minimise_slope (j, αj) (h, αh) pts₁) as ms₁. symmetry in Heqms₁. remember (slope_expr (j, αj) pt ?= slope ms₁) as c₁. symmetry in Heqc₁. destruct c₁; subst ms; simpl. simpl in Hseg, Hep. apply Decidable.not_or in Hseg. destruct Hseg as (Hne, Hseg). subst pts₁. 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. symmetry in Heqc. destruct c; subst ms₁; simpl. simpl in Heqc₁, Hseg, Hep. apply Decidable.not_or in Hseg. destruct Hseg as (Hne₂, Hseg). negation Hne₂. simpl in Heqc₁, Hseg, Hep. injection Hep; clear Hep; intros; subst h αh. apply Qlt_irrefl in Hhk; contradiction. apply Qgt_alt in Heqc. rewrite slope_slope_expr in Heqc; [ idtac | eassumption ]. assumption. simpl in Hseg, Hep. subst pt. apply Qlt_alt in Heqc₁. eapply Qlt_le_trans; [ eassumption | idtac ]. eapply minimised_slope_le; eassumption. subst pts₁. apply Qgt_alt in Heqc₁. 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. symmetry in Heqc. destruct c; subst ms₁; simpl. simpl in Heqc₁, Hseg, Hep. apply Decidable.not_or in Hseg. destruct Hseg as (Hne₂, Hseg). negation Hne₂. simpl in Heqc₁, Hseg, Hep. injection Hep; clear Hep; intros; subst h αh. apply Qlt_irrefl in Hhk; contradiction. apply Qgt_alt in Heqc. rewrite slope_slope_expr in Heqc; [ idtac | eassumption ]. assumption. Qed.
imports: Utf8 QArith Sorting Misc Slope_base ConvexHull ConvexHullMisc