proposition: Lemma msetBSKl A B a : ((a +` A) `\` B) `\ a = A `\` B.
proof: Proof. apply/msetP=> b; rewrite !msetE; case: ifPn; rewrite ?add0n ?subn0 //. by rewrite add1n subn1 subSKn. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap