proposition: Lemma msubset0 A : (A `<=` mset0) = (A == mset0).
proof: Proof. by rewrite eqEmsubset msub0set andbT. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap