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} {xs ys : List α} (h : xs <:+ ys) {i : Nat} (hn : i < xs.length) : xs[i] = ys[ys.length - xs.length + i]

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₂ ↔ take (l₂.length - l₁.length) l₂ ++ l₁ = l₂

theorem List.prefix_take_iff {α : Type u_1} {xs ys : List α} {i : Nat} : xs <+: take i ys ↔ xs <+: ys ∧ xs.length ≤ i

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

theorem List.prefix_take_le_iff {α : Type u_1} {i j : Nat} {xs : List α} (hm : i < xs.length) : take i xs <+: take j xs ↔ i ≤ j

@[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