proposition: Theorem nth_pol_n : ∀ f L c f₁ L₁ fn Ln cn 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) → nth_pol n f₁ L₁ = next_pol fn (β Ln) (γ Ln) cn.
proof: Proof. intros f₁ L₁ c₁ f₂ L₂ fn Ln cn n. intros Hc₁ Hf₂ HL₂ Hfn HLn Hcn. revert f₁ L₁ c₁ f₂ L₂ fn Ln cn Hc₁ Hf₂ HL₂ Hfn HLn Hcn. induction n; intros. simpl in Hfn, HLn; simpl. subst fn Ln f₂ c₁ cn; 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₃ . rewrite <- Hc₁, <- Hf₂, <- HL₂ in Hfn, HLn. eapply IHn; 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