Function vstd::multiset::axiom_len_sub

source · 
pub broadcast proof fn axiom_len_sub<V>(m1: Multiset<V>, m2: Multiset<V>)
Expand description
requires
m2.subset_of(m1),
ensures
(#[trigger] m1.sub(m2).len()) == m1.len() - m2.len(),

The length of the subtraction of two multisets is equal to the difference between the lengths of each individual multiset.