proposition: Theorem minimised_slope_le : ∀ pt₁ pt₂ pts ms, minimise_slope pt₁ pt₂ pts = ms → slope ms <= slope_expr pt₁ pt₂.
proof: Proof. intros pt₁ pt₂ pts ms Hms. revert ms Hms. induction pts as [| pt]; intros. simpl in Hms. subst ms; simpl. apply Qle_refl. simpl in Hms. remember (minimise_slope pt₁ pt pts) as ms₁. remember (slope_expr pt₁ pt₂ ?= slope ms₁) as c. destruct c; subst ms. simpl. symmetry in Heqc; apply Qeq_alt in Heqc. rewrite Heqc. unfold slope at 1; simpl. rewrite slope_slope_expr; [ idtac | symmetry; eassumption ]. apply Qle_refl. simpl. apply Qle_refl. symmetry in Heqc; apply Qgt_alt in Heqc. apply Qlt_le_weak; eassumption. Qed.
imports: Utf8 QArith Sorting Misc Slope_base ConvexHull ConvexHullMisc