exact h_ind (n/2) k
i : Nat
h_ind : ∀ (n k : Nat), getBit (n % 2 ^ k) i = (decide (i < k) && getBit n i)
n k : Nat
this : succ i < succ k ↔ i < k
⊢ getBit (n / 2 % 2 ^ k) i = (decide (i < k) && getBit (n / 2) i)
no goals