[GOAL]
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
src✝¹ : LinearOrderedAddCommMonoidWithTop (WithTop α) := linearOrderedAddCommMonoidWithTop
src✝ : Nontrivial (Option α) := Option.nontrivial
⊢ ∀ (a : WithTop α), a ≠ ⊤ → a + -a = 0
[PROOFSTEP]
rintro (a | a) ha
[GOAL]
case none
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
src✝¹ : LinearOrderedAddCommMonoidWithTop (WithTop α) := linearOrderedAddCommMonoidWithTop
src✝ : Nontrivial (Option α) := Option.nontrivial
ha : none ≠ ⊤
⊢ none + -none = 0
[PROOFSTEP]
exact (ha rfl).elim
[GOAL]
case some
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a✝ b c d : α
src✝¹ : LinearOrderedAddCommMonoidWithTop (WithTop α) := linearOrderedAddCommMonoidWithTop
src✝ : Nontrivial (Option α) := Option.nontrivial
a : α
ha : Option.some a ≠ ⊤
⊢ Option.some a + -Option.some a = 0
[PROOFSTEP]
exact WithTop.coe_add.symm.trans (WithTop.coe_eq_coe.2 (add_neg_self a))
