rw [Nat.getBit, decide_eq_true ‹(n+2)%2 = 1›]
n : Nat
h_ind :
  ∀ {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
hodd : n % 2 = 1
this : (n + 2) % 2 = 1
⊢ getBit (n + 2) 0 = true
no goals