have : n/2 < n := Nat.div_lt_self hpos (Nat.lt_succ_self 1)
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
⊢ n = 0
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
this : n / 2 < n
⊢ n = 0