simp [Order.grlex]
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
⊢ Order.grlex v₁ v₂
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h : algebra.Order.bgrlex v₁ v₂ = true
⊢ if Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂ then True
  else if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False