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