refactor(data/multiset/basic): remove sub lemmas (#9578)
* Remove the multiset sub lemmas that are special cases of lemmas in `algebra/order/sub`
* [This](https://github.com/leanprover-community/mathlib/blob/14c3324143beef6e538f63da9c48d45f4a949604/src/data/multiset/basic.lean#L1513-L1538) gives the list of renamings.
* Use `derive` in `pnat.factors`.
Co-authored-by: Floris van Doorn <fpv@andrew.cmu.edu>
