no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : OrderedCancelAddCommMonoid Γ
inst✝ : NonUnitalNonAssocSemiring R
r : R
x : HahnSeries Γ R
a : Γ
⊢ coeff (x * ↑(single 0) r) a = coeff x a * r
rw [← add_zero a, mul_single_coeff_add, add_zero]