proposition: Theorem nth_c_succ : ∀ n f L f₁ L₁, f₁ = nth_pol (S n) f L → L₁ = nth_ns (S n) f L → nth_c (S n) f L = ac_root (Φq f₁ L₁).
proof: Proof. intros n f L f₁ L₁ Hf₁ HL₁; 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