have _ : one = zero := add_left_eq_zero hw
case intro
a w : Nat
pw : a = a + (w + one)
hw : w + one = zero
⊢ False
case intro
a w : Nat
pw : a = a + (w + one)
hw : w + one = zero
x✝ : one = zero
⊢ False