Commit 2021-10-06 21:14 b4a97675

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