proposition: Theorem ini_lt_fin_pt : ∀ pts ns, Sorted fst_lt pts → lower_convex_hull_points pts = Some ns → fst (ini_pt ns) < fst (fin_pt ns).
proof: Proof. intros pts ns Hsort Hns. unfold lower_convex_hull_points in Hns. destruct pts as [| pt₁ pts]; [ easy | ]. destruct pts as [| pt₂ pts]; [ easy | ]. remember (minimise_slope pt₁ pt₂ pts) as ms eqn:Hms. symmetry in Hms. injection Hns; clear Hns; intros Hns. rewrite <- Hns; simpl. now specialize (beg_lt_end_pt pt₁ pt₂ pts ms Hsort Hms) as H. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base