repeat (
  rw [Order.lex_lt]
  simp
)
case mp
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex_lt v₁ v₂ → Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁

case mpr
n : ℕ
v₁ v₂ : Variables n order.Lex
⊢ Order.lex v₁ v₂ ∧ ¬Order.lex v₂ v₁ → Order.lex_lt v₁ v₂
no goals