case true
x : ℕ
⊢ x + 1 / 2 = x
x : ℕ
b : Bool
⊢ addLsb x b / 2 = x
cases b <;>
    simp only [Nat.add_mul_div_left, addLsb, ← two_mul, add_comm, Nat.succ_pos',
      Nat.mul_div_right, gt_iff_lt, zero_add, cond]
no goals
case true
x : ℕ
⊢ x + 1 / 2 = x
norm_num