proposition: Theorem minimise_slope_le : ∀ pt₁ pt₂ pts₂ ms, Sorted fst_lt [pt₂ … pts₂] → minimise_slope pt₁ pt₂ pts₂ = ms → fst pt₂ <= 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; apply Qle_refl. simpl in Hms. remember (minimise_slope pt₁ pt pts₂) as ms₁. remember (slope_expr pt₁ pt₂ ?= slope ms₁) as c. destruct c; subst ms; simpl; [ idtac | apply Qle_refl | idtac ]. apply Qlt_le_weak. apply Sorted_inv_2 in Hsort. destruct Hsort as (Hlt, Hsort). eapply Qlt_le_trans; [ eassumption | idtac ]. symmetry in Heqms₁. eapply IHpts₂; eassumption. apply Qlt_le_weak. apply Sorted_inv_2 in Hsort. destruct Hsort as (Hlt, Hsort). eapply Qlt_le_trans; [ eassumption | idtac ]. symmetry in Heqms₁. eapply IHpts₂; eassumption. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base