rw [Order.ble_lex_impl]
n✝ : ℕ
v₁ v₂ : Vector ℕ n✝
h✝ : lex_impl v₁ v₂
m : ℕ
a b : Vector ℕ m
property✝¹ property✝ : List.length [] = m
h : lex_impl { val := [], property := property✝¹ } { val := [], property := property✝ }
⊢ algebra.Order.ble_lex_impl { val := [], property := property✝¹ } { val := [], property := property✝ } = true
no goals