case zero => conv => lhs; rw [Nat.pow_zero, Nat.mod_one, Nat.zero_getBit]
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n : Nat
⊢ getBit (n % 2 ^ zero) (succ i) = (decide (succ i < zero) && getBit n (succ i))
no goals