proposition: Theorem L_nat : ∀ f L pts, newton_segments f = Some L → pts = [ini_pt L … oth_pts L ++ [fin_pt L]] → ∀ iq αi, (iq, αi) ∈ pts → ∃ i : nat, iq = Qnat i.
proof: Proof. intros f L pts HL Hpts iq αi Hi. assert (∃ h ah, (iq, αi) = (Qnat h, ah)) as Hnat. eapply points_in_newton_segment_have_nat_abscissa; [ eassumption | idtac ]. subst pts; assumption. destruct Hnat as (h, (ah, Hh)). injection Hh; intros; subst iq ah. exists h; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol