R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
⊢ ∀ (i : ℕ), ↑i < min (order φ) (order ψ) → ↑(coeff R i) (φ + ψ) = 0
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
⊢ min (order φ) (order ψ) ≤ order (φ + ψ)
refine' le_order _ _ _
no goals
R : Type u_1
inst✝ : Semiring R
φ✝ φ ψ : PowerSeries R
⊢ ∀ (i : ℕ), ↑i < min (order φ) (order ψ) → ↑(coeff R i) (φ + ψ) = 0
simp (config := { contextual := true }) [coeff_of_lt_order]