have h_succ := h j.succ (Nat.succ_lt_succ hj)
case mpr
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
m : Nat
h : ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
j : Nat
hj : j < i
⊢ getBit m j = false
case mpr
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
m : Nat
h : ∀ (j : Nat), j < succ i → (decide (j ≥ 1) && getBit m (j - 1)) = false
j : Nat
hj : j < i
h_succ : (decide (succ j ≥ 1) && getBit m (succ j - 1)) = false
⊢ getBit m j = false