proposition: Theorem pol_ord_of_fin_pt : ∀ f L m k αk mk, newton_segments f = Some L → pol_in_K_1_m f m → (Qnat k, αk) = fin_pt L → mk = mh_of_m m αk (ps_poly_nth k f) → αk == mk # m.
proof: Proof. intros f L m k αk mk HL Hm Hini Hmk. subst mk; simpl. unfold mh_of_m; simpl. unfold Qeq; simpl. rewrite Z_div_mul_swap. erewrite qden_αk_is_ps_polydo; eauto with Arith. rewrite Z.div_mul; eauto with Arith. erewrite <- qden_αk_is_ps_polydo; eauto with Arith. eapply den_αk_divides_num_αk_m; 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