proposition: Lemma eq_seq_msetP s s' : reflect (seq_mset s = seq_mset s') (perm_eq s s').
proof: Proof. apply: (iffP idP) => [/permP perm_ss'|eq_ss']. by apply/msetP => a; rewrite !mset_seqE perm_ss'. by apply/allP => a _ /=; rewrite -!mset_seqE eq_ss'. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap