cases n.eq_zero_or_pos
n : Nat
h : ∀ (i : Nat), getBit n i = false
⊢ n = 0
case inl
n : Nat
h : ∀ (i : Nat), getBit n i = false
h✝ : n = 0
⊢ n = 0

case inr
n : Nat
h : ∀ (i : Nat), getBit n i = false
h✝ : n > 0
⊢ n = 0