rw [Order.grlex_lt]
case mpr
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex a b ∧ ¬Order.grlex b a → Order.grlex_lt a b
case mpr
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex a b ∧ ¬Order.grlex b a → Order.grlex a b ∧ ¬Order.grlex b a