feat: Mergesort Stability

[Arleee1]

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

[Shreyas4991]

I think you can always make a PR. I don't see any duplicates yet. Feel free to add it to the MergeSort file in your PR.