proposition: Theorem qden_αj_is_ps_polydo : ∀ f L j αj, newton_segments f = Some L → (Qnat j, αj) = ini_pt L → Qden αj = ps_polydo (ps_poly_nth j f).
proof: Proof. intros f L j αj HL Hini. remember HL as H; clear HeqH. eapply order_in_newton_segment in H; eauto ; [ idtac | left; eauto ]. unfold order in H. remember (ps_poly_nth j f) as ps. remember (series_order (ps_terms ps) 0) as v eqn:Hv . symmetry in Hv. destruct v; [ idtac | discriminate H ]. injection H; clear H; intros H. rewrite <- H; reflexivity. 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