proposition: Lemma msubsetP {A B} : reflect (forall x, A x <= B x) (A `<=` B).
proof: Proof. apply: (iffP forallP)=> // ? x; case: (in_fsetP (finsupp A) x) => //. by rewrite msuppE => /mset_eq0P->. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap