proposition: Lemma perm_enum_basis d : perm_eq [seq s2m (tval s) | s in basis n d] [seq val m | m in [set m : 'X_{1..n < d.+1} | mdeg m == d]].
proof: Proof. Proof using. apply uniq_perm. - rewrite map_inj_in_uniq; first exact: enum_uniq. move=> i j; rewrite !mem_enum => Hi Hj; exact: inj_s2m. - rewrite map_inj_uniq; [exact: enum_uniq | exact: val_inj]. move=> m; apply/mapP/mapP => [[] s | [] mb]. - rewrite mem_enum inE /= => Hsort ->. have mdegs : mdeg (s2m s) = d. rewrite /s2m /mdeg mnm_valK /= big_map enumT -/(index_enum _). by rewrite combclass.sum_count_mem count_predT size_tuple. have mdegsP : (mdeg (s2m s) < d.+1)%N by rewrite mdegs. exists (BMultinom mdegsP) => //. by rewrite mem_enum inE /= mdegs. - rewrite mem_enum inE => /eqP Hmb ->. have Ht : size (m2s mb) == d by rewrite -{2}Hmb size_m2s. exists (Tuple Ht) => /=; last by rewrite s2mK. rewrite mem_enum inE /=; exact: srt_m2s. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition tableau