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

State before:
⊢ ∀ (a b c : Ordering), lex (lex a b) c = lex a (lex b c)
Tactic:
intros a b c
State after:
a b c : Ordering
⊢ lex (lex a b) c = lex a (lex b c)

State before:
a b c : Ordering
⊢ lex (lex a b) c = lex a (lex b c)
Tactic:
cases a <;> simp [lex]
State after:
no goals