simp only [neg, add]
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ add (neg { f := f✝, g := g✝, h := h✝ }) { f := f✝, g := g✝, h := h✝ } = zero
case mk
b c : ℤθ
f✝ g✝ h✝ : ℤ
⊢ { f := -f✝ + f✝, g := -g✝ + g✝, h := -h✝ + h✝ } = zero