Function vstd::multiset::lemma_insert_containment

source · 
pub proof fn lemma_insert_containment<V>(m: Multiset<V>, x: V, y: V)
Expand description
ensures
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.