simp [Order.grlex]
case inl
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex a b
⊢ Order.grlex a b ∨ Order.grlex b a

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a
case inl
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex a b
⊢ (if Order.grlex.elem_sum a < Order.grlex.elem_sum b then True
    else if Order.grlex.elem_sum a = Order.grlex.elem_sum b then if Order.lex a b then True else False else False) ∨
    if Order.grlex.elem_sum b < Order.grlex.elem_sum a then True
    else if Order.grlex.elem_sum b = Order.grlex.elem_sum a then if Order.lex b a then True else False else False

case inr
n : ℕ
a b : Variables n order.GrLex
h✝ : Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a