proposition: Lemma msetU_eq0 A B : (A `|` B == mset0) = (A == mset0) && (B == mset0).
proof: Proof. by rewrite -!msubset0 msubUset. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap