proposition: Theorem exists_oth_pt_nat : ∀ f L pt, newton_segments f = Some L → pt ∈ oth_pts L → ∃ h αh, pt = (Qnat h, αh).
proof: Proof. intros f L pt HL Hpt. destruct pt as ((inum, iden), αi). exists (Z.to_nat inum), αi. unfold newton_segments in HL. remember (points_of_ps_polynom f) as pts. symmetry in Heqpts. eapply oth_pts_in_init_pts in HL; [ idtac | eassumption ]. eapply pt_absc_is_nat in Heqpts; [ idtac | eassumption ]. simpl in Heqpts. rewrite Heqpts; 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