proposition: Theorem den_αj_divides_num_αj_m : ∀ f L j αj m, newton_segments f = Some L → ini_pt L = (Qnat j, αj) → pol_in_K_1_m f m → (Zpos (Qden αj) | Qnum αj * Zpos m)%Z.
proof: Proof. intros f L j αj m HL Hini HinK. apply any_in_K_1_m with (h := j) (αh := αj) 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