proposition: Lemma mset1DE a A b : (a +` A) b = (b == a) + A b.
proof: Proof. by rewrite msetE2 msetnE; case: (b == a). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap