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