Function vstd::multiset::lemma_difference_bottoms_out
source · pub proof fn lemma_difference_bottoms_out<V>(a: Multiset<V>, b: Multiset<V>, x: V)Expand description
ensures
a.count(x) <= b.count(x) ==> a.difference_with(b).count(x) == 0,If the multiplicity of element x is less in multiset a than in multiset b, then the multiplicity
of x in the difference of a and b will be 0.