feat(data/list/basic): some more theorems about sublist (#264)

data/list/basic.lean

@@ -2594,6 +2594,13 @@ theorem diff_sublist_of_sublist : ∀ {l₁ l₂ l₃: list α}, l₁ <+ l₂ 
 | l₁ l₂ (a::l₃) h := by simp
   [diff_cons, diff_sublist_of_sublist (erase_sublist_erase _ h)]
 
+theorem erase_diff_erase_sublist_of_sublist {a : α} : ∀ {l₁ l₂ : list α}, 
+  l₁ <+ l₂ → (l₂.erase a).diff (l₁.erase a) <+ l₂.diff l₁
+| []      l₂ h := by simp [erase_sublist]
+| (b::l₁) l₂ h := if heq : b = a then by simp [heq]
+                  else by simpa [heq, erase_comm a b l₂]
+                  using erase_diff_erase_sublist_of_sublist (erase_sublist_erase b h)
+
 end diff
 
 /- zip & unzip -/

data/list/perm.lean

@@ -519,6 +519,12 @@ else
 have h₂ : a ∉ l₂, from mt (mem_of_perm p).2 h₁,
 by rw [erase_of_not_mem h₁, erase_of_not_mem h₂]; exact p
 
+theorem erase_subperm (a : α) (l : list α) : l.erase a <+~ l :=
+⟨l.erase a, perm.refl _, erase_sublist _ _⟩
+
+theorem erase_subperm_erase {l₁ l₂ : list α} (a : α) (h : l₁ <+~ l₂) : l₁.erase a <+~ l₂.erase a :=
+let ⟨l, hp, hs⟩ := h in ⟨l.erase a, erase_perm_erase _ hp, erase_sublist_erase _ hs⟩
+
 theorem perm_diff_left {l₁ l₂ : list α} (t : list α) (h : l₁ ~ l₂) : l₁.diff t ~ l₂.diff t :=
 by induction t generalizing l₁ l₂ h; simp [*, erase_perm_erase]