Sorting a sum of separated multisets

If every element of a multiset s precedes every element of a multiset t, then sorting s + t lists the sorted elements of s followed by the sorted elements of t. This is how an ordered monomial over an ordered disjoint union of index sets splits into a product of ordered monomials over the two pieces.

theorem Multiset.sort_add {α : Type u_1} (r : α → α → Prop) [DecidableRel r] [IsTrans α r] [Std.Antisymm r] [Std.Total r] {s t : Multiset α} (h : ∀ (a : α), a ∈ s → ∀ (b : α), b ∈ t → r a b) : (s + t).sort r = s.sort r ++ t.sort r

Sorting the sum of two multisets, every element of the first related to every element of the second, appends the two sorted lists.