F : Type ?u.82975
α : Type u_1
β : Type ?u.82981
R : Type ?u.82984
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
hn : Even n
⊢ Odd (n + m)
F : Type ?u.82975
α : Type u_1
β : Type ?u.82981
R : Type ?u.82984
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
hn : Even n
⊢ Odd (m + n)
rw [add_comm]
no goals
F : Type ?u.82975
α : Type u_1
β : Type ?u.82981
R : Type ?u.82984
inst✝¹ : Semiring α
inst✝ : Semiring β
m n : α
hm : Odd m
hn : Even n
⊢ Odd (n + m)
exact hn.add_odd hm