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

State before:
x y : Nat
⊢ 2 * x + 1 ||| 2 * y = 2 * (x ||| y) + 1
Tactic:
simp [or_def, bit1_bitwise_bit0]
State after:
no goals