proposition: Lemma msub1set A a : ([mset a] `<=` A) = (a \in A).
proof: Proof. apply/msubsetP/idP; first by move/(_ a); rewrite msetnxx in_mset. by move=> ainA b; rewrite msetnE; case: eqP => // ->; rewrite -in_mset. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap