Sublists paired with their complements

l.sublists'.revzip pairs each sublist of l with the complementary sublist (List.revzip_sublists'). This file gives its head recursion, the revzip companion of List.sublists'_cons: a sublist of a :: l either omits a, so a joins the complement, or starts with a. [UPSTREAM] candidate for Mathlib/Data/List/Sublists.lean.

Main results

• List.revzip_sublists'_cons: the head recursion of sublists'.revzip.
• List.revzip_singleton: the base case.

@[simp]

theorem List.revzip_singleton {α : Type u_1} (a : α) : [a].revzip = [(a, a)]

theorem List.revzip_sublists'_cons {α : Type u_1} (a : α) (l : List α) : (a :: l).sublists'.revzip = map (Prod.map id fun (x : List α) => a :: x) l.sublists'.revzip ++ map (Prod.map (fun (x : List α) => a :: x) id) l.sublists'.revzip