n : ℕ
⊢ (bif bodd n then 0 else 1) + (bif bodd n then succ (div2 n) else div2 n) * 2 = succ n
n : ℕ
⊢ (bif bodd (succ n) then 1 else 0) + 2 * div2 (succ n) = succ n
simp
n : ℕ
⊢ (bif bodd n then 0 else 1) + (bif bodd n then succ (div2 n) else div2 n) * 2 =
    succ ((bif bodd n then 1 else 0) + 2 * div2 n)
n : ℕ
⊢ (bif bodd n then 0 else 1) + (bif bodd n then succ (div2 n) else div2 n) * 2 = succ n
refine' Eq.trans _ (congr_arg succ (bodd_add_div2 n))
case false
n : ℕ
⊢ 1 + div2 n * 2 = succ (div2 n * 2)

case true
n : ℕ
⊢ succ (div2 n) * 2 = succ (1 + div2 n * 2)
n : ℕ
⊢ (bif bodd n then 0 else 1) + (bif bodd n then succ (div2 n) else div2 n) * 2 =
    succ ((bif bodd n then 1 else 0) + 2 * div2 n)
cases bodd n <;> simp [cond, not]
no goals
case false
n : ℕ
⊢ 1 + div2 n * 2 = succ (div2 n * 2)
rw [Nat.add_comm, Nat.add_succ]
no goals
case true
n : ℕ
⊢ succ (div2 n) * 2 = succ (1 + div2 n * 2)
rw [succ_mul, Nat.add_comm 1, Nat.add_succ]