proposition: Theorem nth_pol_succ : ∀ n f L f₁ L₁ c₁, f₁ = nth_pol n f L → L₁ = nth_ns n f L → c₁ = nth_c n f L → nth_pol (S n) f L = next_pol f₁ (β L₁) (γ L₁) c₁.
proof: Proof. intros n f L f₁ L₁ c₁ Hf₁ HL₁ Hc₁; 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