proposition: Theorem minimise_slope_pts_le : ∀ j αj pt pts ms, minimise_slope (j, αj) pt pts = ms → ∀ h αh, (h, αh) ∈ pts → slope ms <= slope_expr (j, αj) (h, αh).
proof: Proof. intros j αj pt pts ms Hms h αh Hαh. revert pt ms Hms h αh Hαh. induction pts as [| pt₁]; [ contradiction | intros ]. destruct Hαh as [Hαh| Hαh]. subst pt₁. 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. destruct c; subst ms. unfold slope; simpl. rewrite <- minimised_slope; [ idtac | eassumption | reflexivity ]. eapply minimised_slope_le; eassumption. simpl. eapply minimised_slope_le in Heqms₁. symmetry in Heqc; apply Qlt_alt in Heqc. apply Qlt_le_weak. eapply Qlt_le_trans; eassumption. eapply minimised_slope_le in Heqms₁. assumption. 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. symmetry in Heqc. destruct c; subst ms. unfold slope; simpl. rewrite <- minimised_slope; [ idtac | eassumption | reflexivity ]. eapply IHpts; eassumption. simpl. apply Qlt_alt in Heqc. apply Qlt_le_weak. eapply Qlt_le_trans; [ eassumption | idtac ]. eapply IHpts; eassumption. eapply IHpts; eassumption. Qed.
imports: Utf8 QArith Sorting Misc Slope_base ConvexHull ConvexHullMisc