proposition: Theorem nth_c_n : ∀ f₁ L₁ fn Ln n, fn = nth_pol n f₁ L₁ → Ln = nth_ns n f₁ L₁ → nth_c n f₁ L₁ = ac_root (Φq fn Ln).
proof: Proof. intros f₁ L₁ fn Ln n Hfn HLn. revert f₁ L₁ fn Ln Hfn HLn. induction n; intros. simpl in Hfn, HLn; simpl. subst fn Ln; reflexivity. simpl in Hfn, HLn; simpl. remember (ac_root (Φq f₁ L₁)) as c₁ eqn:Hc₁ . remember (next_pol f₁ (β L₁) (γ L₁) c₁) as f₂ eqn:Hf₂ . remember (option_get phony_ns (newton_segments f₂)) as L₂ eqn:HL₂ . apply IHn; assumption. 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