no goals
Γ : Type u_2
R : Type u_1
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
a✝ b : Γ
r✝ : R
a : Γ
r s : R
rs : ↑(single a) r = ↑(single a) s
⊢ r = s
rw [← single_coeff_same a r, ← single_coeff_same a s, rs]