by_cases hb : b = 0
case neg
a b : ℕ
ha : ¬a = 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 pos
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
⊢ (if a = 0 ∨ b = 0 then 0 else ↑1) = if b = 0 then 0 else (if a = 0 then 0 else ↑1) * ↑1