proposition: Theorem den_αh_divides_num_αh_m : ∀ f L h αh m, newton_segments f = Some L → pol_in_K_1_m f m → (Qnat h, αh) ∈ oth_pts L → (Zpos (Qden αh) | Qnum αh * Zpos m)%Z.
proof: Proof. intros f L h αh m HL HinK Hoth. apply any_in_K_1_m with (h := h) (αh := αh) in HinK. destruct HinK as (mh, Hmh). exists mh; assumption. unfold newton_segments in HL. unfold points_of_ps_polynom in HL. eapply oth_pts_in_init_pts in HL; eauto with Arith. 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