rw [Nat.zero_add, ←Nat.shiftLeft_one] at hn
n : Nat
heven : n % 2 = 0
hn : n = 0 + 2 * (n / 2)
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
n : Nat
heven : n % 2 = 0
hn : n = (n / 2) <<< 1
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1