cases i
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
⊢ getBit (Nat.lsb (n + 2)) i = true ↔ getBit (n + 2) i = true ∧ ∀ (j : Nat), j < i → getBit (n + 2) j = false
case zero
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
⊢ getBit (Nat.lsb (n + 2)) zero = true ↔ getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false

case succ
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
n✝ : Nat
⊢ getBit (Nat.lsb (n + 2)) (succ n✝) = true ↔
    getBit (n + 2) (succ n✝) = true ∧ ∀ (j : Nat), j < succ n✝ → getBit (n + 2) j = false