Upstream various lemmas about sublists to Std

[eric-wieser]

As of #301, we will have both List.sublists and List.sublistsFast, where the former is implemented_by the latter.

The proof that this is safe, sublists_eq_sublistsFast, as of leanprover-community/mathlib4#7746 lives in mathlib.
We should upstream the results needed by this lemma (such as List.reverseRecOn) such that sublists_eq_sublistsFast can be in Std instead.