proposition: Theorem end_pt_in : ∀ pt₁ pt₂ pts ms, minimise_slope pt₁ pt₂ pts = ms → fin_pt ms ∈ [pt₂ … pts].
proof: Proof. intros pt₁ pt₂ pts ms Hms. revert pt₁ pt₂ ms Hms. induction pts as [| pt₃]; intros. subst ms; simpl. left; reflexivity. simpl in Hms. remember (minimise_slope pt₁ pt₃ pts) as ms₁. rename Heqms₁ into Hms₁. symmetry in Hms₁. remember (slope_expr pt₁ pt₂ ?= slope ms₁) as c. symmetry in Heqc. remember (fin_pt ms) as pt. destruct c; subst ms; simpl in Heqpt; subst pt. right; eapply IHpts; eassumption. left; reflexivity. right; eapply IHpts; eassumption. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base