b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + bif !b then 1 else 0+1]
b : Bool
n : ℕ
⊢ bit b -[n+1] = -[Nat.bit (!b) n+1]
rw [bit_val, Nat.bit_val]
no goals
b : Bool
n : ℕ
⊢ (2 * -[n+1] + bif b then 1 else 0) = -[2 * n + bif !b then 1 else 0+1]
cases b <;> rfl