case hc
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
⊢ m ≤ m + n
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
⊢ ↑(coeff R (m + n)) (↑(monomial R m) a * φ) = a * ↑(coeff R n) φ
rw [coeff_monomial_mul, if_pos, add_tsub_cancel_left]
no goals
case hc
σ : Type u_2
R : Type u_1
inst✝ : Semiring R
m n : σ →₀ ℕ
φ ψ : MvPowerSeries σ R
a : R
⊢ m ≤ m + n
exact le_add_right le_rfl