no goals
R✝ : Type ?u.4217836
inst✝¹ : Semiring R✝
φ✝ : PowerSeries R✝
R : Type u_1
inst✝ : CommRing R
φ ψ : PowerSeries R
n : ℕ
h : ↑n < order ψ
⊢ ↑(coeff R n) (φ * (1 - ψ)) = ↑(coeff R n) φ
simp [coeff_mul_of_lt_order h, mul_sub]