feat: Mergesort Stability

I am working on a proof that the MergeSort implementation is stable, using the definition below. I am working off of the MergeSort implementation in #372. Would this be a welcome addition to the MergeSort file?

theorem mergeSort_stable
    (xs : List α) (le : α → α → Bool)
    [Std.Total (fun x y => le x y = true)]
    [IsTrans _ (fun x y => le x y = true)] [DecidableEq α] :
    let ys := (mergeSort xs).eval (sortModelNat le)
    ∀ k : α, ys.filter (fun x => le x k && le k x) = xs.filter (fun x => le x k && le k x) := by
  sorry

Start with the MergeSort implementation referenced in issue #372 and inspect how its evaluated result uses sortModelNat le. Compare the proposed mergeSort_stable statement with that implementation and determine whether the filtered equality captures the intended stability. Done means the theorem is accepted without sorry and fits the MergeSort file.