apply eq_zero_of_getBit
case refl.h
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ n / 2 = 0 / 2
case refl.h.h
n : Nat
h : ∀ (i : Nat), getBit 0 i = getBit n i
this : 0 % 2 = n % 2
⊢ ∀ (i : Nat), getBit (n / 2) i = false