proposition: Lemma in_msetB A B a : (a \in A `\` B) = (B a < A a).
proof: Proof. by rewrite -mset_neq0 msetE subn_eq0 ltnNge. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap