F : Type ?u.105241
α : Type u_1
β : Type ?u.105247
R : Type ?u.105250
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Odd b
⊢ Even (a + -b)
F : Type ?u.105241
α : Type u_1
β : Type ?u.105247
R : Type ?u.105250
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Odd b
⊢ Even (a - b)
rw [sub_eq_add_neg]
no goals
F : Type ?u.105241
α : Type u_1
β : Type ?u.105247
R : Type ?u.105250
inst✝ : Ring α
a b : α
n : ℕ
ha : Odd a
hb : Odd b
⊢ Even (a + -b)
exact ha.add_odd hb.neg