have hn : n = 0 + 2 * (n/2) := Eq.symm $ heven ▸ Nat.mod_add_div n 2
n : Nat
heven : n % 2 = 0
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1
n : Nat
heven : n % 2 = 0
hn : n = 0 + 2 * (n / 2)
⊢ Nat.lsb n = Nat.lsb (n / 2) <<< 1