feat(data/multiset/basic): has_ordered_sub multiset (#9566)
* Provide `instance : has_ordered_sub (multiset α)`
* Prove most multiset subtraction lemmas as special cases of `has_ordered_sub` lemmas
* In a subsequent PR I will remove the specialized multiset lemmas
Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
