English
For every integer n, the parity of -n equals the parity of n; parity is invariant under sign change: bodd(-n) = bodd(n).
Русский
Для каждого целого числа n парность числа -n равна парности n; парность сохраняется при смене знака: bodd(-n) = bodd(n).
LaTeX
$$$ ∀ n ∈ \mathbb{Z},\ bodd(-n) = bodd(n). $$$
Lean4
@[simp]
theorem bodd_neg (n : ℤ) : bodd (-n) = bodd n := by
cases n <;> simp only [← negOfNat_eq, bodd_negOfNat, neg_negSucc] <;> simp [bodd]