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