case inr hodd =>
  have := calc
    (n+2) % 2
      = n%2 := Nat.add_mod_right ..
    _ = 1 := hodd
  conv =>
    lhs; lhs
    rw [Nat.lsb_of_odd this]; dsimp [getBit]
    change getBit 0 i; rw [zero_getBit]
  suffices (n+2).getBit 0 = true by
    constructor
    . intro h; cases h
    . intro h; calc
        false = getBit (n+2) 0 := Eq.symm $ h.right 0 i.zero_lt_succ
        _     = true := this
  rw [Nat.getBit, decide_eq_true ‹(n+2)%2 = 1›]
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
hodd : n % 2 = 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
no goals