proposition: Theorem oth_pts_den_1 : ∀ f L, newton_segments f = Some L → List.Forall (λ pt, Qden (fst pt) = 1%positive) (oth_pts L).
proof: Proof. intros f L HL. apply List.Forall_forall. intros pt Hpt. eapply exists_oth_pt_nat in Hpt; [ idtac | eassumption ]. destruct Hpt as (h, (αh, Hpt)). subst pt; 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