proposition: Theorem newton_segments_not_nil : ∀ f L αk r, L = option_get phony_ns (newton_segments f) → fin_pt L = (Qnat r, αk) → (0 < r)%nat → newton_segments f ≠ None.
proof: Proof. intros f L αk r HL Hfin Hr. intros H; rewrite H in HL; subst L. simpl in Hfin. injection Hfin; intros H₁ H₂. rewrite <- Nat2Z.inj_0 in H₂. apply Nat2Z.inj in H₂. rewrite H₂ in Hr. revert Hr; apply Nat.lt_irrefl. 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