proposition: Theorem nth_ns_succ : ∀ n f L f₁, f₁ = nth_pol (S n) f L → nth_ns (S n) f L = option_get phony_ns (newton_segments f₁).
proof: Proof. intros n f L f₁ Hf₁; subst. revert f L. induction n; intros; [ reflexivity | idtac ]. remember (S n) as sn; simpl; subst sn. apply IHn. Qed.
imports: Utf8 QArith NPeano Sorting Misc Field2 Fpolynomial Fsummation Newton ConvexHull Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq F1Prop Q_field PosOrder QbarM