proposition: Theorem degree_pos_imp_has_ns : ∀ f, degree (ps_zerop K) f ≥ 1 → (ps_poly_nth 0 f ≠ 0)%ps → ∃ L, newton_segments f = Some L.
proof: Proof. intros * Hdeg Hnz. specialize (degree_pos_imp_L_not_empty f Hdeg Hnz) as H. remember (newton_segments f) as Ll eqn:HLl . symmetry in HLl. destruct Ll as [L| ]; [ | now exfalso; apply H ]. now exists L. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail RootAnyR