proposition: Theorem slope_slope_expr : ∀ ms pt₁ pt₂ pts, minimise_slope pt₁ pt₂ pts = ms → slope ms == slope_expr pt₁ (fin_pt ms).
proof: Proof. intros ms pt₁ pt₂ pts Hms. unfold slope. rewrite <- Hms at 1. rewrite minimised_slope_beg_pt. reflexivity. Qed.
imports: Utf8 QArith List Slope_base