induction i using Nat.recComplete
case a
n : Nat
h : Nat.lsb n = 0
i : Nat
⊢ getBit n i = false
case a.ind
n : Nat
h : Nat.lsb n = 0
n✝ : Nat
a✝ : ∀ (k : Nat), k < n✝ → getBit n k = false
⊢ getBit n n✝ = false