Theorem: units_ne_neg_self (LeanCourse/Lectures/Lecture10.lean)

State before:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CharZero R
u : Rˣ
⊢ u ≠ -u
Tactic:
sorry
State after:
no goals