proposition: Lemma msetDBA A B C : C `<=` B -> A `+` B `\` C = (A `+` B) `\` C.
proof: Proof. by move=> /msubsetP CB; apply/msetP=> a; rewrite !msetE2 addnBA. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap