proposition: Theorem qden_αh_is_ps_polydo : ∀ f L h αh, newton_segments f = Some L → (Qnat h, αh) ∈ oth_pts L → Qden αh = ps_polydo (ps_poly_nth h f).
proof: Proof. intros f L h αh HL Hoth. remember HL as H; clear HeqH. eapply order_in_newton_segment with (h := h) (αh := αh) in H; eauto with Arith. unfold order in H. remember (ps_poly_nth h 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. right. apply List.in_or_app. left; assumption. 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