feat(data/finsupp): lattice structure on finsupp (#3335)
adds facts about order_isos respecting lattice operations
defines lattice structures on finsupps to N
constructs an order_iso out of finsupp.to_multiset
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
