induction i generalizing n k
n k i : Nat
⊢ getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
case zero
n k : Nat
⊢ getBit (n % 2 ^ k) zero = (decide (zero < k) && getBit n zero)

case succ
n✝ : Nat
n_ih✝ : ∀ (n k : Nat), getBit (n % 2 ^ k) n✝ = (decide (n✝ < k) && getBit n n✝)
n k : Nat
⊢ getBit (n % 2 ^ k) (succ n✝) = (decide (succ n✝ < k) && getBit n (succ n✝))