α✝ : Type u_1
l₁✝ l₂ l₁ l₂✝ : List α✝
a✝ : α✝
h : l₁ <+ l₂✝
⊢ List.reverse l₁ <+ List.reverse l₂✝ ++ [a✝]
α✝ : Type u_1
l₁✝ l₂ l₁ l₂✝ : List α✝
a✝ : α✝
h : l₁ <+ l₂✝
⊢ List.reverse l₁ <+ List.reverse (a✝ :: l₂✝)
rw [reverse_cons]
no goals
α✝ : Type u_1
l₁✝ l₂ l₁ l₂✝ : List α✝
a✝ : α✝
h : l₁ <+ l₂✝
⊢ List.reverse l₁ <+ List.reverse l₂✝ ++ [a✝]
exact sublist_append_of_sublist_left h.reverse
α✝ : Type u_1
l₁ l₂ l₁✝ l₂✝ : List α✝
a✝ : α✝
h : l₁✝ <+ l₂✝
⊢ List.reverse l₁✝ ++ [a✝] <+ List.reverse l₂✝ ++ [a✝]
α✝ : Type u_1
l₁ l₂ l₁✝ l₂✝ : List α✝
a✝ : α✝
h : l₁✝ <+ l₂✝
⊢ List.reverse (a✝ :: l₁✝) <+ List.reverse (a✝ :: l₂✝)
rw [reverse_cons, reverse_cons]
no goals
α✝ : Type u_1
l₁ l₂ l₁✝ l₂✝ : List α✝
a✝ : α✝
h : l₁✝ <+ l₂✝
⊢ List.reverse l₁✝ ++ [a✝] <+ List.reverse l₂✝ ++ [a✝]
exact h.reverse.append_right _