Function vstd::multiset::lemma_update_different
source · pub proof fn lemma_update_different<V>(m: Multiset<V>, v1: V, mult: nat, v2: V)Expand description
requires
v1 != v2,m.update(v1, mult).count(v2) == m.count(v2),The multiset resulting from updating a value v1 in a multiset m to multiplicity mult will
not change the multiplicities of any other values in m.