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?

[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.