simp [Order.grlex] at ab bc
n : ℕ
a b c : Variables n order.GrLex
ab : Order.grlex a b
bc : Order.grlex b c
⊢ if Order.grlex.elem_sum a < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False
n : ℕ
a b c : Variables n order.GrLex
ab :
  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
bc :
  if Order.grlex.elem_sum b < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum b = Order.grlex.elem_sum c then if Order.lex b c then True else False else False
⊢ if Order.grlex.elem_sum a < Order.grlex.elem_sum c then True
  else if Order.grlex.elem_sum a = Order.grlex.elem_sum c then if Order.lex a c then True else False else False