cases Nat.mod_two_eq_zero_or_one n
n : Nat
⊢ getBit (Nat.lsb n) 0 = getBit n 0
case inl
n : Nat
h✝ : n % 2 = 0
⊢ getBit (Nat.lsb n) 0 = getBit n 0

case inr
n : Nat
h✝ : n % 2 = 1
⊢ getBit (Nat.lsb n) 0 = getBit n 0