Function vstd::multiset::lemma_multiset_properties

forall |m: Multiset<V>, v: V, mult: nat| #[trigger] m.update(v, mult).count(v) == mult,

forall |m: Multiset<V>, v1: V, mult: nat, v2: V| {
    v1 != v2 ==> #[trigger] m.update(v1, mult).count(v2) == m.count(v2)
},

forall |m: Multiset<V>| {
    (#[trigger] m.len() == 0 <==> m =~= Multiset::empty())
        && (#[trigger] m.len() > 0 ==> exists |v: V| 0 < m.count(v))
},

forall |m: Multiset<V>, x: V, y: V| {
    0 < #[trigger] m.insert(x).count(y) <==> x == y || 0 < m.count(y)
},

forall |m: Multiset<V>, x: V| #[trigger] m.insert(x).count(x) == m.count(x) + 1,

forall |m: Multiset<V>, x: V, y: V| {
    0 < m.count(y) ==> 0 < #[trigger] m.insert(x).count(y)
},

forall |m: Multiset<V>, x: V, y: V| {
    x != y ==> #[trigger] m.count(y) == #[trigger] m.insert(x).count(y)
},

forall |m: Multiset<V>, x: V| #[trigger] m.insert(x).len() == m.len() + 1,

forall |a: Multiset<V>, b: Multiset<V>, x: V| {
    #[trigger] a.intersection_with(b).count(x)
        == min(a.count(x) as int, b.count(x) as int)
},

forall |a: Multiset<V>, b: Multiset<V>| {
    #[trigger] a.intersection_with(b).intersection_with(b) == a.intersection_with(b)
},

forall |a: Multiset<V>, b: Multiset<V>| {
    #[trigger] a.intersection_with(a.intersection_with(b)) == a.intersection_with(b)
},

forall |a: Multiset<V>, b: Multiset<V>, x: V| {
    #[trigger] a.difference_with(b).count(x) == clip(a.count(x) - b.count(x))
},

forall |a: Multiset<V>, b: Multiset<V>, x: V| {
    #[trigger] a.count(x) <= #[trigger] b.count(x)
        ==> (#[trigger] a.difference_with(b)).count(x) == 0
},