Theorem: Ordering.opp_inj (GMLInit/Data/Basic.lean)

State before:
x y : Ordering
⊢ x.opp = y.opp → x = y
Tactic:
intro h
State after:
x y : Ordering
h : x.opp = y.opp
⊢ x = y

State before:
x y : Ordering
h : x.opp = y.opp
⊢ x = y
Tactic:
rw [←opp_opp x, ←opp_opp y, h]
State after:
no goals