have : n/2 = 0 := eq_zero_of_getBit (n:=n/2) (λ i => h i.succ)
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this : n / 2 < n
⊢ n = 0
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this✝ : n / 2 < n
this : n / 2 = 0
⊢ n = 0