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