have := calc
  n+2 = (n/2)*2 + 2 := by rw [Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero heven)]
  _   = (n/2 + 1)*2 := Eq.symm $ Nat.add_mul ..
  _   = (n/2 + 1) <<< 1 := by rw [Nat.mul_comm, Nat.shiftLeft_one]
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
heven : n % 2 = 0
⊢ getBit (Nat.lsb (n + 2)) (succ i) = true ↔
    getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false
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
heven : n % 2 = 0
this : n + 2 = (n / 2 + 1) <<< 1
⊢ getBit (Nat.lsb (n + 2)) (succ i) = true ↔
    getBit (n + 2) (succ i) = true ∧ ∀ (j : Nat), j < succ i → getBit (n + 2) j = false