proposition: Theorem min_slope_lt_after_k : ∀ j αj k αk pt pts ms, Sorted fst_lt pts → minimise_slope (j, αj) pt pts = ms → fin_pt ms = (k, αk) → ∀ h αh, (h, αh) ∈ pts → k < h → slope ms < slope_expr (j, αj) (h, αh).
proof: Proof. intros j αj k αk pt pts ms Hsort Hms Hep h αh Hαh Hkh. revert pt ms Hms Hep h Hαh Hkh. induction pts as [| pt₁]; [ contradiction | intros ]. destruct Hαh as [Hαh| Hαh]. subst pt₁. remember Hms as H; clear HeqH. apply end_pt_in in Hms. rewrite Hep in Hms. destruct Hms as [Hms| Hms]. subst pt. simpl in H. remember (minimise_slope (j, αj) (h, αh) pts) as ms₁. symmetry in Heqms₁. remember (slope_expr (j, αj) (k, αk) ?= slope ms₁) as c. destruct c; subst ms. simpl in Hep |- *. apply minimise_slope_le in Heqms₁; [ idtac | assumption ]. rewrite Hep in Heqms₁. apply Qle_not_lt in Heqms₁; contradiction. simpl in Hep |- *; clear Hep. symmetry in Heqc; apply Qlt_alt in Heqc. eapply Qlt_le_trans; [ eassumption | idtac ]. eapply minimised_slope_le; eassumption. symmetry in Heqc; apply Qgt_alt in Heqc. apply minimise_slope_le in Heqms₁; [ idtac | assumption ]. rewrite Hep in Heqms₁; simpl in Heqms₁. apply Qle_not_lt in Heqms₁. contradiction. destruct Hms as [Hms| Hms]. injection Hms; clear Hms; intros; subst h αh. apply Qlt_irrefl in Hkh; contradiction. eapply Sorted_hd in Hsort; [ idtac | eassumption ]. simpl in Hsort. eapply Qlt_trans in Hsort; [ idtac | eassumption ]. apply Qlt_irrefl in Hsort; contradiction. simpl in Hms. remember (minimise_slope (j, αj) pt₁ pts) as ms₁. symmetry in Heqms₁. remember (slope_expr (j, αj) pt ?= slope ms₁) as c. destruct c; subst ms. simpl in Hep |- *. unfold slope; simpl. rewrite <- minimised_slope; [ idtac | eassumption | reflexivity ]. eapply IHpts; try eassumption. destruct pts as [| pts₁]; [ constructor | idtac ]. apply Sorted_inv_2 in Hsort; destruct Hsort; assumption. simpl in Hep |- *. subst pt. symmetry in Heqc; apply Qlt_alt in Heqc. eapply Qlt_le_trans; [ eassumption | idtac ]. eapply minimise_slope_pts_le; eassumption. eapply IHpts; try eassumption. destruct pts as [| pts₁]; [ constructor | idtac ]. apply Sorted_inv_2 in Hsort; destruct Hsort; assumption. Qed.
imports: Utf8 QArith Sorting Misc Slope_base ConvexHull ConvexHullMisc