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. It is transitive (List.Nodup.pair_sublist_trans), so it is a strict order on the whole type (List.Nodup.isStrictOrder_pair_sublist) in which elements off the list are related to nothing; two distinct members are ordered one way or the other (List.pair_sublist_or_pair_sublist), and a duplicate-free list whose members lie in another, each pair in the same order there, is a sublist of it (List.sublist_of_forall_pair_sublist).

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

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

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

theorem List.Nodup.pair_sublist_trans {α : Type u_1} {a b : α} {l : List α} {c : α} (hl : l.Nodup) (hab : [a, b].Sublist l) (hbc : [b, c].Sublist l) : [a, c].Sublist l

theorem List.Nodup.isStrictOrder_pair_sublist {α : Type u_1} {l : List α} (hl : l.Nodup) : IsStrictOrder α fun (a b : α) => [a, b].Sublist l

theorem List.sublist_of_forall_pair_sublist {α : Type u_1} {p q : List α} (hp : p.Nodup) (hq : q.Nodup) (hpq : p ⊆ q) (h : ∀ (a b : α), [a, b].Sublist p → [a, b].Sublist q) : p.Sublist q

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

theorem List.pair_sublist_or_pair_sublist {α : Type u_1} {a b : α} {l : List α} [DecidableEq α] (ha : a ∈ l) (hb : b ∈ l) (hab : a ≠ b) : [a, b].Sublist l ∨ [b, a].Sublist l

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