no goals
m✝ n✝ m n : ℕ
hn : Odd n
hm : Even m
⊢ m % 2 + (m + n) % 2 = 1
rw [even_iff.1 hm, odd_iff.1 (hm.add_odd hn)]
no goals
m✝ n✝ m n : ℕ
hn : Odd n
hm : Odd m
⊢ m % 2 + (m + n) % 2 = 1
rw [odd_iff.1 hm, even_iff.1 (hm.add_odd hn)]