α✝ : Type u_1
l₁ l₂ l : List α✝
h : l₁ ++ l <+ l₂ ++ l
this : reverse (l₁ ++ l) <+ reverse (l₂ ++ l)
⊢ l₁ <+ l₂
α✝ : Type u_1
l₁ l₂ l : List α✝
h : l₁ ++ l <+ l₂ ++ l
⊢ l₁ <+ l₂
have := h.reverse
α✝ : Type u_1
l₁ l₂ l : List α✝
h : l₁ ++ l <+ l₂ ++ l
this : l₁ <+ l₂
⊢ l₁ <+ l₂
α✝ : Type u_1
l₁ l₂ l : List α✝
h : l₁ ++ l <+ l₂ ++ l
this : reverse (l₁ ++ l) <+ reverse (l₂ ++ l)
⊢ l₁ <+ l₂
simp only [reverse_append, append_sublist_append_left, reverse_sublist] at this
no goals
α✝ : Type u_1
l₁ l₂ l : List α✝
h : l₁ ++ l <+ l₂ ++ l
this : l₁ <+ l₂
⊢ l₁ <+ l₂
exact this