 Additive multiset union

The operation adding multiset multiplicities pointwise. Its result retains all occurrences from both operands. Some sources use the name multiset union instead for pointwise maximum, so a contract should state which operation is meant.