no goals
m n : ℤ
⊢ bodd (m * n) = (bodd m && bodd n)
cases' m with m m <;> cases' n with n n <;>
simp only [ofNat_eq_coe, ofNat_mul_negSucc, negSucc_mul_ofNat, ofNat_mul_ofNat,
           negSucc_mul_negSucc] <;>
simp only [negSucc_coe, bodd_neg, bodd_coe, ←Nat.bodd_mul]