case inr hm =>
  have : m/2 < m := Nat.div_lt_self hm (Nat.lt_succ_self 1)
  exact bitext (m:=m/2) (n:=n/2) (λ i => h i.succ)
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