proposition: Theorem minimise_slope_lt_seg : ∀ pt₁ pt₂ pt₃ pts ms₂, Sorted fst_lt [pt₁; pt₂; pt₃ … pts] → minimise_slope pt₁ pt₃ pts = ms₂ → HdRel fst_lt pt₂ (oth_pts ms₂).
proof: Proof. intros pt₁ pt₂ pt₃ pts ms₂ Hsort Hms₂. revert pt₁ 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. symmetry in Heqc. destruct c. subst ms₂; simpl. constructor. apply Sorted_inv_2 in Hsort. destruct Hsort as (_, Hsort). apply Sorted_inv_2 in Hsort. destruct Hsort; assumption. subst ms₂; constructor. move Hms₂ at top; subst ms₄. eapply IHpts; [ idtac | eassumption ]. eapply Sorted_minus_3rd; [ 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