vstd::set_lib

Function lemma_set_difference_len

Source 
pub broadcast proof fn lemma_set_difference_len<A>(a: Set<A>, b: Set<A>)
Expand description
requires
a.finite(),
b.finite(),
ensures
(#[trigger] a.difference(b).len() + b.difference(a).len() + a.intersect(b).len()
    == (a + b).len()) && (a.difference(b).len() == a.len() - a.intersect(b).len()),

The length of the set difference A \ B added to the length of the set difference B \ A added to the length of the intersection A ∩ B is equal to the length of the union A + B.

The length of the set difference A \ B is equal to the length of A minus the length of the intersection A ∩ B.