min_max): maximum is a fold, bounded prod (#8543)

Commit

4 years ago

feat(data/list/min_max): maximum is a fold, bounded prod (#8543) Also provide the same lemmas for multiset.

Author

pechersky

Parents