rw [if_neg, if_neg hb, if_neg ha]
case neg
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1
case neg
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ↑1 = ↑1 * ↑1

case neg.hnc
a b : ℕ
ha : ¬a = 0
hb : ¬b = 0
⊢ ¬(a = 0 ∨ b = 0)