proposition: Lemma msetB1E a A b : (A `\ a) b = (A b) - (b == a).
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