case zero =>
  rw [Nat.lsb_getBit_zero]
  constructor
  show (n+2).getBit 0 = true → (n+2).getBit zero = true ∧ ∀ j, j < 0 → _ 
  . intro h; apply And.intro h ?_
    intro _ hj; cases hj
  show (n+2).getBit zero = true ∧ _ → (n+2).getBit zero = true 
  . exact And.left
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
no goals