feat: List.insertP and lemmas

[fgdorais]

List.insertP is a generalized, tail-recursive version of the insert step in insertion-sort. Sample use:

def insertionSort [LT α] [DecidableRel (α:=α) (· < ·)] (l : List α) := 
  l.foldl (fun s a => s.insertP (a < ·) a) [] -- fully tail recursive and stable!

It will be useful to streamline and optimize ac_rfl once moved to Std.

PS: Perhaps someone has a better name?

[joehendrix]

I don't have a specific objection to insertP, but we are working on triaging what parts of Std can and should be moved to Lean core (with further polishing) to provide a good new user experience.

As such I'd like to hold off introducing new operations unless they enhance existing capabilities or are needed for high-priority tactics.

[fgdorais]

The ac_rfl move has been canceled so there is no immediate need for this. It's still a useful addition so I'm reluctant to close but closing might be better than rotting.