match a, b with
  | ⟨[], p⟩, ⟨[], q⟩       => rw [Order.lex_impl]
                              split
                              simp
                              simp at *
  | ⟨x::xs, p⟩, ⟨y::ys, q⟩ => rw [Order.lex_impl]
                              simp [Or.comm]
                              rw [Order.lex_impl]
                              split
                              simp
                              split
                              split
                              simp [Or.comm]
                              apply aux (m-1) (tail ⟨x::xs, p⟩) (tail ⟨y::ys, q⟩)
                              simp at *
                              rename_i eq neq heq₁ heq₂
                              have s_eq := Eq.symm eq
                              have eq_1 := Eq.symm heq₁.left
                              have eq_2 := Eq.symm heq₂.left
                              rw [eq_1, eq_2] at s_eq
                              contradiction
                              split
                              simp at *
                              rename_i neq eq heq₁ heq₂
                              have s_eq := Eq.symm eq
                              have eq_1 := heq₁.left
                              have eq_2 := heq₂.left
                              rw [eq_1, eq_2] at s_eq
                              contradiction
                              simp at *
                              rename_i heq₁ heq₂
                              have eq_1 := heq₁.left
                              have eq_2 := heq₂.left
                              rw [eq_1, eq_2]
                              simp [Nat.le_total]
n : ℕ
v₁ v₂ : Variables n order.Lex
m : ℕ
a b : Vector ℕ m
⊢ Order.lex_impl a b ∨ Order.lex_impl b a
no goals