∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (m n : σ →₀ ℕ) (φ : MvPowerSeries σ R),
  MvPolynomial.coeff m ((MvPowerSeries.trunc' R n) φ) = if m ≤ n then (MvPowerSeries.coeff m) φ else 0