proposition: Theorem in_pol_in_pts : ∀ f pts h hv hps, pts = points_of_ps_polynom f → hps = List.nth h (al f) 0%ps → order hps = qfin hv → (Qnat h, hv) ∈ pts.
proof: Proof. intros f pts h hv hps Hpts Hhps Hv. eapply in_ppl_in_pts; try eassumption; try reflexivity. apply Nat.le_0_l. rewrite Nat.sub_0_r; 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