proposition: Lemma mem_msetD1 a A : a \notin A -> A `\ a = A.
proof: Proof. move=> /mset_eq0P aA; apply/msetP => x; rewrite !msetE. by have [->|] := altP eqP; rewrite ?aA ?subn0. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap