a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0

case H
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ 2 ≠ 0
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ div2 (bit b n) = n
rw [bit_val, div2_val, add_comm, Int.add_mul_ediv_left, (_ : (_ / 2 : ℤ) = 0), zero_add]
case false
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ (bif false then 1 else 0) / 2 = 0

case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0

case H
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ 2 ≠ 0
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ (bif b then 1 else 0) / 2 = 0

case H
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ 2 ≠ 0
cases b
no goals
case false
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ (bif false then 1 else 0) / 2 = 0
simp
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ ofNat (1 / 2) = 0
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ (bif true then 1 else 0) / 2 = 0
show ofNat _ = _
no goals
case true
a b : ℤ
n✝ : ℕ
n : ℤ
⊢ ofNat (1 / 2) = 0
rw [Nat.div_eq_zero] <;> simp
no goals
case H
a b✝ : ℤ
n✝ : ℕ
b : Bool
n : ℤ
⊢ 2 ≠ 0
decide