no goals
m n : ℕ
⊢ bodd (subNatNat m n) = xor (Nat.bodd m) (Nat.bodd n)
apply subNatNat_elim m n fun m n i => bodd i = xor m.bodd n.bodd <;>
intros i j <;>
simp only [Int.bodd, Int.bodd_coe, Nat.bodd_add] <;>
cases Nat.bodd i <;> simp