simp [h]
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

case inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : if Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂ then if Order.lex v₁ v₂ then True else False else False
⊢ algebra.Order.bgrlex v₁ v₂ = true
case inl.inl
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : True
h : algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
le : algebra.Order.bgrlex.elem_sum v₁ ≤ algebra.Order.bgrlex.elem_sum v₂
⊢ ¬Order.lex v₁ v₂ → False

case inl.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h : True
h✝ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
⊢ algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False

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