have leq := Nat.le_of_not_lt nleq
case inr.inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
nleq : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
neq₁ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
neq₂ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
⊢ False
case inr.inr.inr
n✝ : ℕ
v₁ v₂ : Variables n✝ order.GrLex
nleq : ¬Order.grlex.elem_sum v₁ < Order.grlex.elem_sum v₂
neq₁ : ¬Order.grlex.elem_sum v₁ = Order.grlex.elem_sum v₂
neq₂ : ¬algebra.Order.bgrlex.elem_sum v₁ = algebra.Order.bgrlex.elem_sum v₂
h : algebra.Order.bgrlex.elem_sum v₂ ≤ algebra.Order.bgrlex.elem_sum v₁ → False
leq : Order.grlex.elem_sum v₂ ≤ Order.grlex.elem_sum v₁
⊢ False