English
For all integers n, n = (if n is odd then 1 else 0) + 2 · div2(n).
Русский
Для любого n ∈ ℤ верно: n = (если n нечетно, то 1, иначе 0) + 2 · div2(n).
LaTeX
$$$$ \forall n \in \mathbb{Z},\ \operatorname{cond}(\operatorname{bodd} n)\,1\,0 + 2 \cdot \operatorname{div2} n = n. $$$$
Lean4
theorem bodd_add_div2 : ∀ n, cond (bodd n) 1 0 + 2 * div2 n = n
| (n : ℕ) => by
rw [show (cond (bodd n) 1 0 : ℤ) = (cond (bodd n) 1 0 : ℕ) by cases bodd n <;> rfl]
exact congr_arg ofNat n.bodd_add_div2
| -[n+1] => by
refine Eq.trans ?_ (congr_arg negSucc n.bodd_add_div2)
dsimp [bodd]; cases Nat.bodd n <;> dsimp [cond, not, div2, Int.mul]
· change -[2 * Nat.div2 n+1] = _
rw [zero_add]
· rw [zero_add, add_comm]
rfl
