case inl hm => 
  cases hm; apply Eq.symm
  apply eq_zero_of_getBit
  exact λ i => zero_getBit i.succ ▸ (h i.succ).symm
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
hm : m = 0
⊢ m / 2 = n / 2
no goals