case negSucc.negSucc
m n : ℕ
⊢ Nat.bodd (Nat.succ (m + n) + 1) = Nat.bodd (m + 1 + (n + 1))
m n : ℤ
⊢ bodd (m + n) = xor (bodd m) (bodd n)
cases' m with m m <;>
cases' n with n n <;>
simp only [ofNat_eq_coe, ofNat_add_negSucc, negSucc_add_ofNat,
           negSucc_add_negSucc, bodd_subNatNat] <;>
simp only [negSucc_coe, bodd_neg, bodd_coe, ←Nat.bodd_add, Bool.xor_comm, ←Nat.cast_add]
no goals
case negSucc.negSucc
m n : ℕ
⊢ Nat.bodd (Nat.succ (m + n) + 1) = Nat.bodd (m + 1 + (n + 1))
rw [←Nat.succ_add, add_assoc]