show (n+2).getBit 0 = true → (n+2).getBit zero = true ∧ ∀ j, j < 0 → _
case mp
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 (n + 2) 0 = true → getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) 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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) 0 = true
case mp
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 (n + 2) 0 = true → getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < 0 → getBit (n + 2) 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
⊢ (getBit (n + 2) zero = true ∧ ∀ (j : Nat), j < zero → getBit (n + 2) j = false) → getBit (n + 2) 0 = true