proposition: Theorem in_seg_in_pts : ∀ pt pt₁ pt₂ pts, pt ∈ oth_pts (minimise_slope pt₁ pt₂ pts) → pt ∈ [pt₂ … pts].
proof: Proof. intros pt pt₁ pt₂ pts Hpt. revert pt₂ Hpt. induction pts as [| pt₃]; intros; [ contradiction | idtac ]. simpl in Hpt. remember (minimise_slope pt₁ pt₃ pts) as ms₃. remember (slope_expr pt₁ pt₂ ?= slope ms₃) as c. destruct c; simpl in Hpt. destruct Hpt as [Hpt| Hpt]. subst pt; left; reflexivity. right; subst ms₃; apply IHpts; assumption. contradiction. right; subst ms₃; apply IHpts; assumption. Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base