proposition: Theorem exists_fin_pt_nat : ∀ f L, newton_segments f = Some L → ∃ i αi, fin_pt L = (Qnat i, αi).
proof: Proof. intros f L HL. remember (fin_pt L) as ii. destruct ii 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. apply ini_fin_ns_in_init_pts in HL. destruct HL as (_, HL). eapply pt_absc_is_nat in Heqpts; [ idtac | eassumption ]. rewrite <- Heqii in Heqpts; 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