no goals
n : ℤ
⊢ bodd (-n) = bodd n
cases n with
| ofNat =>
  rw [←negOfNat_eq, bodd_negOfNat]
  simp
| negSucc n =>
  rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
  change (!Nat.bodd n) = !(bodd n)
  rw [bodd_coe]
case ofNat
a✝ : ℕ
⊢ Nat.bodd a✝ = bodd (ofNat a✝)
case ofNat
a✝ : ℕ
⊢ bodd (-ofNat a✝) = bodd (ofNat a✝)
rw [←negOfNat_eq, bodd_negOfNat]
no goals
case ofNat
a✝ : ℕ
⊢ Nat.bodd a✝ = bodd (ofNat a✝)
simp
case negSucc
n : ℕ
⊢ (!Nat.bodd n) = bodd -[n+1]
case negSucc
n : ℕ
⊢ bodd (- -[n+1]) = bodd -[n+1]
rw [neg_negSucc, bodd_coe, Nat.bodd_succ]
case negSucc
n : ℕ
⊢ (!Nat.bodd n) = !bodd ↑n
case negSucc
n : ℕ
⊢ (!Nat.bodd n) = bodd -[n+1]
change (!Nat.bodd n) = !(bodd n)
no goals
case negSucc
n : ℕ
⊢ (!Nat.bodd n) = !bodd ↑n
rw [bodd_coe]