proposition: Theorem pt₁_bef_seg : ∀ pt₁ pt₂ pts pth, Sorted fst_lt [pt₁; pt₂ … pts] → pth ∈ oth_pts (minimise_slope pt₁ pt₂ pts) → fst pt₁ < fst pth.
proof: Proof. intros pt₁ pt₂ pts pth Hsort Hh. revert pt₁ pt₂ pth Hsort Hh. induction pts as [| pt₃]; intros; [ contradiction | idtac ]. simpl in Hh. remember (minimise_slope pt₁ pt₃ pts) as ms₃. remember (slope_expr pt₁ pt₂ ?= slope ms₃) as c. symmetry in Heqc. destruct c. simpl in Hh. destruct Hh as [Hh| Hh]. subst pth. eapply Sorted_hd; [ eassumption | left; reflexivity ]. subst ms₃. eapply IHpts; [ idtac | eassumption ]. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. contradiction. subst ms₃. eapply IHpts; [ idtac | eassumption ]. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. 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