intro n k
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
⊢ ∀ (n k : Nat), Nat.lsb n <<< k = Nat.lsb (n <<< k)
this : ∀ (n : Nat), 2 * Nat.lsb n = Nat.lsb (2 * n)
n k : Nat
⊢ Nat.lsb n <<< k = Nat.lsb (n <<< k)