Function vstd::multiset::axiom_count_le_len
source · pub broadcast proof fn axiom_count_le_len<V>(m: Multiset<V>, v: V)Expand description
ensures
#[trigger] m.count(v) <= #[trigger] m.len(),The count for any given value v in a multiset m must be less than or equal to the length of m.