proposition: Lemma s2mK n (m : 'X_{1..n}): s2m (m2s m) = m.
proof: Proof. apply/mnmP=> i; rewrite mnmE /m2s /=. rewrite count_flatten sumnE !big_map (bigD1 i) //=. rewrite -sum1_count /= big_nseq_cond eqxx iter_succn. rewrite add0n big1 ?addn0 // => j ne_ji; apply/count_memPn. by apply/negP=> /nseqP [/esym/eqP]; rewrite (negbTE ne_ji). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(order fingroup perm ssralg zmodp poly ssrint) mathcomp(matrix vector) mathcomp(bigenough) ssrcomplements freeg