proposition: Theorem in_pts_in_pol : ∀ f pts h hv hps def, pts = points_of_ps_polynom f → (Qnat h, hv) ∈ pts → hps = List.nth h (al f) def → hps ∈ al f ∧ order hps = qfin hv.
proof: Proof. intros f pts h hv hps def Hpts Hhhv Hhps. eapply in_pts_in_psl; try eassumption. simpl; rewrite Nat.sub_0_r, Nat2Z.id; eassumption. 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