Function vstd::multiset::lemma_insert_containment

0 < m.insert(x).count(y) <==> x == y || 0 < m.count(y),

If you insert element x into multiset m, then element y maps to a count greater than 0 if and only if x==y or y already mapped to a count greater than 0 before the insertion of x.