Theorem: Ordering.lex_assoc''' (Katydid/Std/Ordering.lean)

State before:
a b c : Ordering
⊢ lex (lex lt b) c = lex lt (lex b c)
Tactic:
rfl
State after:
no goals

State before:
a b c : Ordering
⊢ lex (lex gt b) c = lex gt (lex b c)
Tactic:
rfl
State after:
no goals