proposition: Lemma subset_msetBLR A B C : (msubset (A `\` B) C) = (A `<=` B `+` C).
proof: Proof. apply/msubsetP/msubsetP => [] sABC a; by have := sABC a; rewrite !msetE ?leq_subLR. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap