case inl heven =>
  have := calc
    n+2 = (n/2)*2 + 2 := by rw [Nat.div_mul_cancel (Nat.dvd_of_mod_eq_zero heven)]
    _   = (n/2 + 1)*2 := Eq.symm $ Nat.add_mul ..
    _   = (n/2 + 1) <<< 1 := by rw [Nat.mul_comm, Nat.shiftLeft_one]
  simp only [
    this, ←Nat.lsb_shiftLeft,
    Nat.succ_eq_add_one,
    ←Nat.shiftRight_getBit,
    Nat.shiftLeft_shiftRight_self,
    Nat.shiftLeft_getBit
  ]
  suffices ∀ (m : Nat), (∀ j, j < i → m.getBit j = false) ↔ (∀ j, j < i.succ → (decide (j≥1) && m.getBit (j-1)) = false) by
    rw [←this]; exact h_ind
  intro m; constructor
  show (∀ j, j < i → m.getBit j = false) → (∀ j, j < i.succ → (decide (j≥ 1) && m.getBit (j-1)) = false)
  . intro h j hj
    cases j
    case zero =>
      rw [decide_eq_false (p:=zero ≥ 1) (by decide), Bool.false_and]
    case succ j =>
      have : j < i := lt_of_succ_lt_succ hj
      rw [decide_eq_true (p:=j.succ ≥ 1) j.zero_lt_succ, Bool.true_and, Nat.succ_sub_one]
      exact h j this
  show (∀ j, j < i.succ → (decide (j ≥ 1) && m.getBit (j-1)) = false) → _
  . intro h j hj
    have h_succ := h j.succ (Nat.succ_lt_succ hj)
    conv at h_succ =>
      rw [decide_eq_true (p:=j.succ≥1) j.zero_lt_succ, Bool.true_and, Nat.succ_sub_one]
    exact h_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
i : Nat
heven : n % 2 = 0
⊢ 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