Theorem Cardinal.mk_multiset_of_nonempty

Modification history