case intro
F : Type ?u.101923
α : Type u_1
β : Type ?u.101929
R : Type ?u.101932
inst✝ : Ring α
a b : α
n : ℕ
k : α
hk : a = 2 * k + 1
⊢ Odd (-a)
F : Type ?u.101923
α : Type u_1
β : Type ?u.101929
R : Type ?u.101932
inst✝ : Ring α
a b : α
n : ℕ
hp : Odd a
⊢ Odd (-a)
obtain ⟨k, hk⟩ := hp
case intro
F : Type ?u.101923
α : Type u_1
β : Type ?u.101929
R : Type ?u.101932
inst✝ : Ring α
a b : α
n : ℕ
k : α
hk : a = 2 * k + 1
⊢ -a = 2 * -(k + 1) + 1
case intro
F : Type ?u.101923
α : Type u_1
β : Type ?u.101929
R : Type ?u.101932
inst✝ : Ring α
a b : α
n : ℕ
k : α
hk : a = 2 * k + 1
⊢ Odd (-a)
use -(k + 1)
no goals
case intro
F : Type ?u.101923
α : Type u_1
β : Type ?u.101929
R : Type ?u.101932
inst✝ : Ring α
a b : α
n : ℕ
k : α
hk : a = 2 * k + 1
⊢ -a = 2 * -(k + 1) + 1
rw [mul_neg, mul_add, neg_add, add_assoc, two_mul (1 : α), neg_add, neg_add_cancel_right, ←
  neg_add, hk]