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