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