Further lemmas about List.IsSuffix / List.IsPrefix / List.IsInfix.

These are in a separate file from most of the lemmas about List.IsSuffix as they required importing more lemmas about natural numbers, and use omega.

theorem List.IsSuffix.getElem {α : Type u_1} {x y : List α} (h : x <:+ y) {n : Nat} (hn : n < x.length) : x[n] = y[y.length - x.length + n]

theorem List.isSuffix_iff {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ ↔ l₁.length ≤ l₂.length ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i + l₂.length - l₁.length]? = some l₁[i]

theorem List.isInfix_iff {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+: l₂ ↔ ∃ (k : Nat), l₁.length + k ≤ l₂.length ∧ ∀ (i : Nat) (h : i < l₁.length), l₂[i + k]? = some l₁[i]

theorem List.suffix_iff_eq_append {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ ↔ List.take (l₂.length - l₁.length) l₂ ++ l₁ = l₂

theorem List.prefix_take_iff {α : Type u_1} {x y : List α} {n : Nat} : x <+: List.take n y ↔ x <+: y ∧ x.length ≤ n

theorem List.suffix_iff_eq_drop {α✝ : Type u_1} {l₁ l₂ : List α✝} : l₁ <:+ l₂ ↔ l₁ = List.drop (l₂.length - l₁.length) l₂

theorem List.prefix_take_le_iff {α : Type u_1} {m n : Nat} {L : List α} (hm : m < L.length) : List.take m L <+: List.take n L ↔ m ≤ n

@[simp]

theorem List.append_left_sublist_self {α : Type u_1} {xs : List α} (ys : List α) : (xs ++ ys).Sublist ys ↔ xs = []

@[simp]

theorem List.append_right_sublist_self {α : Type u_1} (xs : List α) {ys : List α} : (xs ++ ys).Sublist xs ↔ ys = []

theorem List.append_sublist_of_sublist_left {α : Type u_1} {xs ys zs : List α} (h : zs.Sublist xs) : (xs ++ ys).Sublist zs ↔ ys = [] ∧ xs = zs

theorem List.append_sublist_of_sublist_right {α : Type u_1} {xs ys zs : List α} (h : zs.Sublist ys) : (xs ++ ys).Sublist zs ↔ xs = [] ∧ ys = zs