Theorem: Nat.zero_or_one_of_log2' (Algdata/Data/Nat/Bits.lean)

State before:
n✝ : Nat
h : log2' (n✝ + 2) = 0
⊢ n✝ + 2 = 0 ∨ n✝ + 2 = 1
Tactic:
cases log2'_div2 _ ▸ h
State after:
no goals