proposition: Theorem minimised_slope : ∀ pt₁ pt₂ pt pts ms, minimise_slope pt₁ pt pts = ms → pt₂ = fin_pt ms → slope ms == slope_expr pt₁ pt₂.
proof: Proof. intros pt₁ pt₂ pt pts ms Hms Hkps. unfold slope; subst. rewrite minimised_slope_beg_pt; reflexivity. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base