proposition: Theorem seg_bef_end_pt : ∀ pt₁ pt₂ pts ms₁ hq αh kq αk, Sorted fst_lt [pt₁; pt₂ … pts] → minimise_slope pt₁ pt₂ pts = ms₁ → (hq, αh) ∈ oth_pts ms₁ → (kq, αk) = fin_pt ms₁ → hq < kq.
proof: Proof. fix IHpts 3. intros pt₁ pt₂ pts ms₁ hq αh kq αk Hsort Hms₁ Hseg Hend. destruct pts as [| pt₃]; [ subst ms₁; contradiction | idtac ]. simpl in Hms₁. remember (minimise_slope pt₁ pt₃ pts) as ms₂. symmetry in Heqms₂. remember (slope_expr pt₁ pt₂ ?= slope ms₂) as c. symmetry in Heqc. destruct c. subst ms₁; simpl in Hseg, Hend. destruct Hseg as [Hseg| Hseg]. apply Sorted_inv_1 in Hsort. apply Sorted_hd with (pt₂ := (kq, αk)) in Hsort. subst pt₂; assumption. rewrite Hend. eapply end_pt_in; eassumption. eapply IHpts with (pts := pts); try eassumption. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. subst ms₁; simpl in Hseg, Hend; contradiction. subst ms₁; simpl in Hseg, Hend. eapply IHpts with (pts := pts); try 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