match a, b with
 | ⟨[], _⟩, ⟨[], _⟩       => rw [Order.ble_lex_impl]
 | ⟨x::xs, _⟩, ⟨y::ys, _⟩ => rw [Order.ble_lex_impl]
                             split;rfl
                             split
                             rw [lex_impl] at h
                             simp at h
                             split at h
                             apply Order.ble_eq_true_of_lex h
                             rename_i heq₁ heq₂ neq eq
                             simp at heq₁ heq₂
                             have eq₁ := heq₁.left
                             have eq₂ := heq₂.left
                             simp at neq
                             rw [eq₁, eq₂] at eq
                             contradiction
                             rw [lex_impl] at h
                             simp at h
                             split at h
                             rename_i heq₁ heq₂ neq eq
                             simp at heq₁ heq₂
                             have eq₁ := heq₁.left
                             have eq₂ := heq₂.left
                             simp at neq
                             rw [eq₁, eq₂] at eq
                             contradiction
                             simp
                             rename_i heq₁ heq₂ _ _
                             simp at heq₁ heq₂
                             have eq₁ := Eq.symm heq₁.left
                             have eq₂ := Eq.symm heq₂.left
                             rwa [eq₁, eq₂]
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
h : lex_impl a b
⊢ algebra.Order.ble_lex_impl a b = true
no goals