proposition: Theorem puiseux_series_algeb_closed : ∀ (f : polynomial (puiseux_series α)), degree (ps_zerop K) f ≥ 1 → ∃ s, (ps_pol_apply f s = 0)%ps.
proof: Proof. intros f Hdeg. destruct (ps_zerop _ (ps_poly_nth 0 f)) as [Hz| Hnz]. exists 0%ps. unfold ps_pol_apply, apply_poly, apply_lap; simpl. unfold ps_poly_nth, ps_lap_nth in Hz; simpl in Hz. remember (al f) as la eqn:Hla . symmetry in Hla. destruct la as [| a]; [ reflexivity | simpl in Hz; simpl ]. rewrite rng_mul_0_r, rng_add_0_l; assumption. specialize (degree_pos_imp_has_ns f Hdeg Hnz) as (L, HL). remember (ac_root (Φq f L)) as c eqn:Hc . remember (next_pol f (β L) (γ L) c) as f₁ eqn:Hf₁ . rewrite Hc in Hf₁. specialize (f₁_has_root HL Hnz Hf₁) as (s₁, Hs₁). exists (ps_monom c (γ L) + ps_monom 1%K (γ L) * s₁)%ps. eapply f₁_root_f_root; eauto . rewrite <- Hc. reflexivity. Qed.
imports: Utf8 QArith NPeano Sorting Misc SlopeMisc Slope_base QbarM NbarM Field2 Fpolynomial Fsummation Newton ConvexHullMisc ConvexHull PolyConvexHull NotInSegment Power_series Puiseux_series Ps_add Ps_mul Ps_div PSpolynomial Puiseux_base AlgCloCharPol CharactPolyn F1Eq PosOrder F1Prop InK1m Q_field RootHeadTail RootAnyR