Sublists across a block of one symbol, and pair sublists as positional order

Two additions to the List.Sublist API.

• Stripping an unmatched edge. A list whose head is not a is a sublist of a :: r exactly when it is a sublist of r (List.sublist_cons_iff_of_head?_ne, the Iff form of List.Sublist.of_cons_of_ne), hence also across a left block replicate m a or a right block replicate n b (List.sublist_replicate_append_iff_of_head?_ne, List.sublist_append_replicate_iff_of_getLast?_ne). [UPSTREAM] candidates beside List.sublist_cons_iff.
• Pair sublists as positional order. On a Nodup list, [a, b] <+ l says exactly that a and b are members with a at a strictly earlier index (List.pair_sublist_iff_idxOf_lt): the pair-sublist relation is the strict linear order a duplicate-free list carries.

theorem List.sublist_cons_iff_of_head?_ne {α : Type u_1} {a : α} {l r : List α} (h : l.head? ≠ some a) : l.Sublist (a :: r) ↔ l.Sublist r

A list whose head is not a is a sublist of a :: r exactly when it is a sublist of r: the Iff form of List.Sublist.of_cons_of_ne.

theorem List.sublist_replicate_append_iff_of_head?_ne {α : Type u_1} {a : α} {l r : List α} {m : ℕ} (h : l.head? ≠ some a) : l.Sublist (replicate m a ++ r) ↔ l.Sublist r

A list whose head is not a is a sublist of replicate m a ++ r exactly when it is a sublist of r.

theorem List.sublist_append_replicate_iff_of_getLast?_ne {α : Type u_1} {b : α} {l r : List α} {n : ℕ} (h : l.getLast? ≠ some b) : l.Sublist (r ++ replicate n b) ↔ l.Sublist r

A list whose last element is not b is a sublist of r ++ replicate n b exactly when it is a sublist of r.

theorem List.pair_sublist_of_idxOf_lt {α : Type u_1} {a b : α} {l : List α} [DecidableEq α] (ha : a ∈ l) (hb : b ∈ l) (h : idxOf a l < idxOf b l) : [a, b].Sublist l

theorem List.idxOf_lt_of_pair_sublist {α : Type u_1} {a b : α} {l : List α} [DecidableEq α] (hnd : l.Nodup) (h : [a, b].Sublist l) : idxOf a l < idxOf b l

theorem List.pair_sublist_iff_idxOf_lt {α : Type u_1} {a b : α} {l : List α} [DecidableEq α] (hnd : l.Nodup) : [a, b].Sublist l ↔ a ∈ l ∧ b ∈ l ∧ idxOf a l < idxOf b l

On a Nodup list, the pair-sublist relation is the strict positional order.

theorem List.IsInfix.mem_of_idxOf_le_of_le {α : Type u_1} {a b : α} {l : List α} [DecidableEq α] {m : List α} {z : α} (hm : m <:+: l) (hnd : l.Nodup) (ha : a ∈ m) (hb : b ∈ m) (hz : z ∈ l) (haz : idxOf a l ≤ idxOf z l) (hzb : idxOf z l ≤ idxOf b l) : z ∈ m

On a Nodup list, an element positioned between two elements of an infix belongs to the infix.