proposition: Lemma in_msetn n a' a : a \in msetn n a' = (n > 0) && (a == a').
proof: Proof. by rewrite in_mset msetE; case: (a == a'); rewrite ?andbT ?andbF. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap