contradiction
case h.left
R G : Type
inst✝² : Ring R
inst✝¹ : Group G
inst✝ : DecidableEq G
p : FormalSum R G
a : R
g : G
hyp : p ≈ [(a, g)] ∧ a ≠ 0
this✝ : FormalSum.coords p = FormalSum.coords [(a, g)]
h : a = 0
this : a ≠ 0
⊢ False
no goals