Function vstd::multiset::lemma_difference_count
source · pub proof fn lemma_difference_count<V>(a: Multiset<V>, b: Multiset<V>, x: V)Expand description
ensures
a.difference_with(b).count(x) == clip(a.count(x) - b.count(x)),The multiplicity of an element x in the difference of multisets a and b will be
equal to the difference of the counts of x in a and b, or 0 if this difference is negative.