proposition: Theorem next_has_ns : ∀ f L c f₁, newton_segments f = Some L → c = ac_root (Φq f L) → f₁ = next_pol f (β L) (γ L) c → (ps_poly_nth 0 f₁ ≠ 0)%ps → newton_segments f₁ ≠ None.
proof: Proof. intros f L c f₁ HL Hc Hf₁ Hnz₁. eapply next_has_root_0_or_newton_segments in HL; try reflexivity. simpl in HL; rewrite <- Hc, <- Hf₁ in HL. destruct HL; [ contradiction | assumption ]. 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