proposition: Lemma msupp_mesym k : perm_eq (msupp 's_k) [seq mesym1 h | h : {set 'I_n} <- enum {set 'I_n} & #|h| == k].
proof: Proof. rewrite mesymE; apply/(perm_trans (msupp_sum _ _ _))=> /=. + by rewrite /index_enum -enumT enum_uniq. + move=> h1 h2 _ _ ne_h1h2 m /=; rewrite !msuppX !mem_seq1. apply/negbTE/negP=> /andP[/eqP->] /eqP /inj_mesym1. by move/eqP; rewrite (negbTE ne_h1h2). rewrite /index_enum -enumT /= (eq_map (fun h => msuppX _ (mesym1 h))). by rewrite (map_comp (cons^~ [::])) flatten_seq1. 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