proposition: Theorem ord_coeff_non_zero_in_newt_segm : ∀ f L h αh hps, newton_segments f = Some L → (Qnat h, αh) ∈ [ini_pt L … oth_pts L ++ [fin_pt L]] → hps = List.nth h (al f) 0%ps → (order_coeff hps ≠ 0)%K.
proof: Proof. intros f L h αh hps HL Hh Hhps. unfold order_coeff. remember (series_order (ps_terms hps) 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]. apply series_order_iff in Hn. destruct Hn; assumption. remember (points_of_ps_polynom f) as pts eqn:Hpts . remember Hpts as H; clear HeqH. eapply in_pts_in_pol in H; try eassumption. destruct H as (Hhp, Hhhv). unfold order in Hhhv. rewrite Hn in Hhhv; discriminate Hhhv. unfold newton_segments in HL. rewrite <- Hpts in HL. destruct Hh as [Hh| Hh]. apply ini_fin_ns_in_init_pts in HL. rewrite Hh in HL. destruct HL; eassumption. apply List.in_app_or in Hh. destruct Hh as [Hh| [Hh| ]]; [ idtac | idtac | contradiction ]. eapply oth_pts_in_init_pts in HL; eassumption. apply ini_fin_ns_in_init_pts in HL. rewrite Hh in HL. destruct HL; eassumption. 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