no goals
R : Type u_1
inst✝ : CommSemiring R
m n : ℕ
φ : PowerSeries R
⊢ Polynomial.coeff (trunc n φ) m = if m < n then ↑(coeff R m) φ else 0
simp [trunc, Polynomial.coeff_sum, Polynomial.coeff_monomial, Nat.lt_succ_iff]