proposition: Theorem den_αk_divides_num_αk_m : ∀ f L k αk m, newton_segments f = Some L → pol_in_K_1_m f m → fin_pt L = (Qnat k, αk) → (Zpos (Qden αk) | Qnum αk * Zpos m)%Z.
proof: Proof. intros f L k αk m HL HinK Hini. apply any_in_K_1_m with (h := k) (αh := αk) in HinK. destruct HinK as (mh, Hmh). exists mh; assumption. unfold newton_segments in HL. unfold points_of_ps_polynom in HL. apply ini_fin_ns_in_init_pts in HL. destruct HL; rewrite <- Hini; 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