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