Theorem exists_multiset_prod_cons_le_and_prod_not_le

Modification history