proposition: Theorem nth_ns_n : ∀ f L c f₁ L₁ fn Ln cn nfn n, c = ac_root (Φq f L) → f₁ = next_pol f (β L) (γ L) c → L₁ = option_get phony_ns (newton_segments f₁) → fn = nth_pol n f L → Ln = nth_ns n f L → cn = ac_root (Φq fn Ln) → nfn = next_pol fn (β Ln) (γ Ln) cn → nth_ns n f₁ L₁ = option_get phony_ns (newton_segments nfn).
proof: Proof. intros f L c f₁ L₁ fn Ln cn nfn n. intros Hc Hf₁ HL₁ Hfn HLn Hcn Hnfn. revert f L c f₁ L₁ fn Ln cn nfn Hc Hf₁ HL₁ Hfn HLn Hcn Hnfn. induction n; intros. simpl in Hfn, HLn; simpl. subst fn Ln nfn f₁ L₁ c cn. reflexivity. simpl in Hfn, HLn; simpl. rewrite <- Hc, <- Hf₁, <- HL₁ in Hfn, HLn. 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₂. rename HeqL₂ into HL₂. eapply IHn with (c := c₁); eauto . 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