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.