proposition: Theorem ns_in_init_pts : ∀ pts L pt, lower_convex_hull_points pts = Some L → pt ∈ [ini_pt L … oth_pts L ++ [fin_pt L]] → pt ∈ pts.
proof: Proof. intros pts L pt HL Hpt. destruct Hpt as [Hpt| Hpt]. subst pt. apply ini_fin_ns_in_init_pts; assumption. apply List.in_app_or in Hpt. destruct Hpt as [Hpt| Hpt]. eapply oth_pts_in_init_pts; eassumption. destruct Hpt as [Hpt| ]; [ idtac | contradiction ]. subst pt. apply ini_fin_ns_in_init_pts; assumption. 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