Theorem: Nat.bit1_div_two (Extra/Nat/Bitwise.lean)

State before:
x : Nat
⊢ (2 * x + 1) / 2 = x
Tactic:
omega
State after:
no goals