proposition: Theorem in_ch_in_pts : ∀ pts pt₁ pt₂ s, lower_convex_hull_points pts = Some (mkns pt₁ pt₂ s) → pt₁ ∈ pts ∧ pt₂ ∈ pts.
proof: Proof. intros pts pt₁ pt₂ s Hhs. unfold lower_convex_hull_points in Hhs. destruct pts as [| pt₃]; [ discriminate Hhs | idtac ]. destruct pts as [| pt₄]; [ discriminate Hhs | idtac ]. injection Hhs; clear Hhs; intros; subst pt₁ pt₂ s. split; [ now rewrite minimised_slope_beg_pt; left | ]. remember (minimise_slope pt₃ pt₄ pts) as ms₁. symmetry in Heqms₁. apply end_pt_in in Heqms₁. right; assumption. Qed.
imports: Utf8 QArith Sorting Misc Slope_base ConvexHull ConvexHullMisc