proposition: Theorem f₁_eq_x_min_β₁_comp : ∀ f β₁ γ₁ c₁, (next_pol f β₁ γ₁ c₁ = POL [ps_monom 1%K (- β₁)] * f ∘ (POL [ps_monom 1%K γ₁] * POL [ps_monom c₁ 0; 1%ps … []]))%pspol.
proof: Proof. intros f β₁ γ₁ c₁. apply lap_f₁_eq_x_min_β₁_comp; reflexivity. Qed.
imports: Utf8 QArith NPeano Sorted ConvexHullMisc ConvexHull PolyConvexHull Field2 Misc Newton NbarM QbarM SplitList Fsummation Fpolynomial Power_series Puiseux_series Ps_add Ps_mul Ps_div Ps_add_compat PSpolynomial Puiseux_base CharactPolyn AlgCloCharPol