proposition: Theorem minimised_slope_beg_pt : ∀ pt₁ pt₂ pts, ini_pt (minimise_slope pt₁ pt₂ pts) = pt₁.
proof: Proof. intros pt₁ pt₂ pts. revert pt₁ pt₂. induction pts as [| pt]; intros; [ reflexivity | simpl ]. remember (minimise_slope pt₁ pt pts) as ms. remember (slope_expr pt₁ pt₂ ?= slope ms) as c. symmetry in Heqc. destruct c; simpl; [ reflexivity | reflexivity | idtac ]. subst ms; apply IHpts. Qed.
imports: Utf8 QArith List Slope_base