Function vstd::multiset::lemma_insert_non_decreasing

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

If multiset m maps element y to a multiplicity greater than 0, then inserting any element x into m will not cause y to map to a multiplicity of 0. This is a way of saying that inserting x will not cause any counts to decrease, because it accounts both for when x == y and when x != y.