case inr hpos =>
  have : n/2 < n := Nat.div_lt_self hpos (Nat.lt_succ_self 1)
  have : n/2 = 0 := eq_zero_of_getBit (n:=n/2) (λ i => h i.succ)
  have : n%2 = 0 := eq_mod2_of_decide (n:=0) (h 0)
  exact eq_of_div_mod_two_eq (n:=0) ‹n/2=0› ‹n%2=0›
n : Nat
h : ∀ (i : Nat), getBit n i = false
hpos : n > 0
⊢ n = 0
no goals