proposition: Lemma msetBD1K A B a : A `<=` B -> A a < B a -> a +` (B `\` (a +` A)) = B `\` A.
proof: Proof. move=> /msubsetP AB ABa; apply/msetP => b; rewrite !msetE. by case: ifP => //= /eqP->; rewrite !add1n subnSK. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap