proposition: Lemma msetE2 A B a : ((A `+` B) a = A a + B a) * ((A `|` B) a = maxn (A a) (B a)) * ((A `&` B) a = minn (A a) (B a)) * ((A `\` B) a = (A a) - (B a)).
proof: Proof. rewrite !fsfunE !inE !msuppE -!mset_neq0; case: ifPn => //. by rewrite negb_or !negbK => /andP [/eqP-> /eqP->]. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap