induction n using recBase2 generalizing i
n i : Nat
⊢ getBit (Nat.lsb n) i = true ↔ getBit n i = true ∧ ∀ (j : Nat), j < i → getBit n j = false
case zero
i : Nat
⊢ getBit (Nat.lsb 0) i = true ↔ getBit 0 i = true ∧ ∀ (j : Nat), j < i → getBit 0 j = false

case one
i : Nat
⊢ getBit (Nat.lsb 1) i = true ↔ getBit 1 i = true ∧ ∀ (j : Nat), j < i → getBit 1 j = false

case div2
n✝ : Nat
a✝ :
  ∀ {i : Nat},
    getBit (Nat.lsb (n✝ / 2 + 1)) i = true ↔
      getBit (n✝ / 2 + 1) i = true ∧ ∀ (j : Nat), j < i → getBit (n✝ / 2 + 1) j = false
i : Nat
⊢ getBit (Nat.lsb (n✝ + 2)) i = true ↔ getBit (n✝ + 2) i = true ∧ ∀ (j : Nat), j < i → getBit (n✝ + 2) j = false