have : m / 2 = n / 2 := by
  cases m.eq_zero_or_pos
  case inl hm => 
    cases hm; apply Eq.symm
    apply eq_zero_of_getBit
    exact λ i => zero_getBit i.succ ▸ (h i.succ).symm
  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
⊢ m = n
m n : Nat
h : ∀ (i : Nat), getBit m i = getBit n i
this✝ : m % 2 = n % 2
this : m / 2 = n / 2
⊢ m = n