proposition: Lemma msetB_eq0 (A B : {mset K}) : (A `\` B == mset0) = (A `<=` B).
proof: Proof. apply/mset_eqP/msubsetP => AB a; by have := AB a; rewrite !msetE -subn_eq0 => /eqP. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap