ι : Type ?u.197416
α : Type u_1
β : Type ?u.197422
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
b0 : 0 ≤ b
a0 : 0 ≤ -b
⊢ -b = b
ι : Type ?u.197416
α : Type u_1
β : Type ?u.197422
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
a0 : 0 ≤ a
b0 : 0 ≤ b
h : a = -b
⊢ a = b
subst a
ι : Type ?u.197416
α : Type u_1
β : Type ?u.197422
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
b0 : 0 ≤ b
a0 : 0 ≤ -b
this : b = 0
⊢ -b = b
ι : Type ?u.197416
α : Type u_1
β : Type ?u.197422
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
b0 : 0 ≤ b
a0 : 0 ≤ -b
⊢ -b = b
have : b = 0 := le_antisymm (neg_nonneg.1 a0) b0
no goals
ι : Type ?u.197416
α : Type u_1
β : Type ?u.197422
inst✝ : LinearOrderedField α
b c d : α
n : ℤ
b0 : 0 ≤ b
a0 : 0 ≤ -b
this : b = 0
⊢ -b = b
rw [this, neg_zero]