have contr := lex_le_total a b
n : ℕ
a b : Variables n order.GrLex
⊢ Order.grlex a b ∨ Order.grlex b a
n : ℕ
a b : Variables n order.GrLex
contr : Order.lex a b ∨ Order.lex b a
⊢ Order.grlex a b ∨ Order.grlex b a