proposition: Theorem pol_ord_of_oth_pt : ∀ f L m h αh mh, newton_segments f = Some L → pol_in_K_1_m f m → (Qnat h, αh) ∈ oth_pts L → mh = mh_of_m m αh (ps_poly_nth h f) → αh == mh # m.
proof: Proof. intros f L m h αh mh HL Hm Hfin Hmh. subst mh; simpl. unfold mh_of_m; simpl. unfold Qeq; simpl. rewrite Z_div_mul_swap. erewrite qden_αh_is_ps_polydo; eauto with Arith. rewrite Z.div_mul; eauto with Arith. erewrite <- qden_αh_is_ps_polydo; eauto with Arith. eapply den_αh_divides_num_αh_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