proposition: Theorem Sorted_hd : ∀ (pt₁ pt₂ : Q * Q) pts, Sorted fst_lt [pt₁ … pts] → pt₂ ∈ pts → fst pt₁ < fst pt₂.
proof: Proof. intros pt₁ pt₂ pts Hsort Hpt. revert pt₁ pt₂ Hsort Hpt. induction pts as [| pt]; intros; [ contradiction | idtac ]. apply Sorted_inv_2 in Hsort. destruct Hsort as (Hlt, Hsort). destruct Hpt as [Hpt| Hpt]; [ subst pt; assumption | idtac ]. eapply Qlt_trans; [ eassumption | idtac ]. apply IHpts; assumption. Qed.
imports: Utf8 QArith Sorting Misc ConvexHull Slope_base