contradiction
case inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
h✝¹ : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
h✝ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
h : False
⊢ algebra.Order.bgrlex v₁ v₂ = true
no goals