proposition: Theorem nth_g_order_pos : ∀ f L h, newton_segments f = Some L → (order (ps_lap_nth h (g_lap_of_ns f L)) > 0)%Qbar.
proof: Proof. intros f L h HL. destruct (lt_dec h (length (g_lap_of_ns f L))) as [Hlt| Hge]. eapply each_power_of_y₁_in_g_has_coeff_pos_ord; try eassumption. reflexivity. unfold g_of_ns; simpl. unfold ps_lap_nth. apply list_nth_in; assumption. apply Nat.nlt_ge in Hge. unfold ps_lap_nth. rewrite List.nth_overflow; [ idtac | assumption ]. rewrite order_0; constructor. Qed.
imports: Utf8 QArith NPeano Sorted Misc QbarM SplitList Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull Puiseux_base Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial AlgCloCharPol CharactPolyn F1Eq PosOrder InK1m