proposition: Theorem next_ns_in_f : ∀ f L c f₁ L₁, newton_segments f = Some L → c = ac_root (Φq f L) → f₁ = next_pol f (β L) (γ L) c → L₁ = option_get phony_ns (newton_segments f₁) → (ps_poly_nth 0 f₁ ≠ 0)%ps → newton_segments f₁ = Some L₁.
proof: Proof. intros f L c f₁ L₁ HL Hc Hf₁ HL₁ Hnz₁. eapply next_has_ns in HL; try eassumption . destruct (newton_segments f₁) as [L'₁| ]; [ | easy ]. now f_equal. 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