Function vstd::multiset::lemma_intersection_count
source · pub proof fn lemma_intersection_count<V>(a: Multiset<V>, b: Multiset<V>, x: V)Expand description
ensures
a.intersection_with(b).count(x) == min(a.count(x) as int, b.count(x) as int),The multiplicity of an element x in the intersection of multisets a and b will be the minimum
count of x in either a or b.