proposition: Theorem pol_ord_of_ini_pt : ∀ f L m j αj mj, newton_segments f = Some L → pol_in_K_1_m f m → (Qnat j, αj) = ini_pt L → mj = mh_of_m m αj (ps_poly_nth j f) → αj == mj # m.
proof: Proof. intros f L m j αj mj HL Hm Hini Hmj. subst mj; simpl. unfold mh_of_m; simpl. unfold Qeq; simpl. rewrite Z_div_mul_swap. erewrite qden_αj_is_ps_polydo; eauto with Arith. rewrite Z.div_mul; eauto with Arith. erewrite <- qden_αj_is_ps_polydo; eauto with Arith. eapply den_αj_divides_num_αj_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