proposition: Theorem minimise_slope_seg_sorted : ∀ pt₁ pt₂ pts ms₁, Sorted fst_lt [pt₁; pt₂ … pts] → minimise_slope pt₁ pt₂ pts = ms₁ → Sorted fst_lt (oth_pts ms₁).
proof: Proof. intros pt₁ pt₂ pts ms₁ Hsort Hms₁. revert pt₁ pt₂ ms₁ Hsort Hms₁. induction pts as [| pt₃]; intros. subst ms₁; constructor. simpl in Hms₁. remember (minimise_slope pt₁ pt₃ pts) as ms₂. symmetry in Heqms₂. remember (slope_expr pt₁ pt₂ ?= slope ms₂)%Q as c. destruct c. subst ms₁; simpl. constructor. eapply IHpts; [ idtac | eassumption ]. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. eapply minimise_slope_lt_seg; eassumption. subst ms₁; constructor. 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