proposition: Theorem hull_seg_vert_in_init_pts : ∀ pts hs, lower_convex_hull_points pts = Some hs → ini_pt hs ∈ pts ∧ fin_pt hs ∈ pts.
proof: Proof. intros pts hs Hnp. destruct pts as [| pt₁]; [ discriminate Hnp | idtac ]. destruct pts as [| pt₂]; [ discriminate Hnp | idtac ]. injection Hnp; clear Hnp; intros Hnp; subst hs. rewrite minimised_slope_beg_pt. split; [ left; reflexivity | idtac ]. remember List.In as f; simpl; subst f. right; eapply end_pt_in; reflexivity. Qed.
imports: Utf8 QArith Sorted NPeano ConvexHull ConvexHullMisc Misc NbarM QbarM Newton PolyConvexHull Field2 Fpolynomial PSpolynomial Puiseux_base Power_series Puiseux_series Ps_div Slope_base