cases m.eq_zero_or_pos
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
⊢ m / 2 = n / 2
case inl
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
h✝ : m = 0
⊢ m / 2 = n / 2

case inr
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this : m % 2 = n % 2
h✝ : m > 0
⊢ m / 2 = n / 2