proposition: Theorem beg_lt_end_pt : ∀ pt₁ pt₂ pts ms, Sorted fst_lt [pt₁; pt₂ … pts] → minimise_slope pt₁ pt₂ pts = ms → fst (ini_pt ms) < fst (fin_pt ms).
proof: Proof. intros pt₁ pt₂ pts ms Hsort Hms. revert pt₁ pt₂ ms Hsort Hms. induction pts as [| pt₃]; intros. subst ms; simpl. eapply Sorted_hd; [ eassumption | left; reflexivity ]. simpl in Hms. remember (minimise_slope pt₁ pt₃ pts) as ms₁ eqn:Hms₁ . remember (slope_expr pt₁ pt₂ ?= slope ms₁) as c. symmetry in Heqc. symmetry in Hms₁. rewrite slope_slope_expr in Heqc; [ idtac | eassumption ]. destruct c. subst ms; simpl. rewrite <- minimised_slope_beg_pt in |- * at 1. rewrite <- Hms₁. eapply IHpts; [ idtac | reflexivity ]. eapply Sorted_minus_2nd; [ idtac | eassumption ]. intros x y z H₁ H₂; eapply Qlt_trans; eassumption. subst ms; simpl. 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. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base