proposition: Lemma Kostka_mnmwiden n (m : 'X_{1..n.+1}) : KostkaMon la m = KostkaMon la (mnmwiden m).
proof: Proof. rewrite /KostkaMon /KostkaTab. pose ext_fun := fun (t : tabsh la) => [seq [seq (widen_ord (leqnSn n.+1) i) | i <- r] | r <- t]. have extP t : is_tab_of_shape la (ext_fun t). rewrite /is_tab_of_shape /=; apply/andP; split. - by rewrite -incr_tab ?tabshP. - rewrite -(shape_tabsh t) /shape /ext_fun -map_comp. by apply/eqP/eq_map => s; rewrite /= size_map. have ext_inj : injective (fun t => TabSh (extP t)). move=> u v [] /= H; apply val_inj => /=. have:= H => /(congr1 size); rewrite !size_map => Hsz. apply (eq_from_nth (x0 := [::])) => // r Hr. move: H => /(congr1 (fun t => nth [::] t r)). rewrite !(nth_map [::]) -?Hsz // => H. have:= H => /(congr1 size); rewrite !size_map => Hsz1. apply (eq_from_nth (x0 := ord0)) => // c Hc. move: H => /(congr1 (fun t => nth ord0 t c)). rewrite !(nth_map ord0) -?Hsz1 //= => /(congr1 val) /= Heq. by apply val_inj. rewrite -(card_imset _ ext_inj); congr #|pred_of_set _|. apply/setP => /= t2; rewrite inE /=. apply/imsetP/eqP => /= [[t ] | Hm]. - rewrite inE /= => /eqP Hm /(congr1 val)/= Heq. rewrite /eval; apply eq_from_tnth => i; rewrite tnth_mktuple. case: (ssrnat.ltnP i n.+1) => Hi. + rewrite [RHS](tnth_nth 0) /= nth_rcons size_tuple Hi -{}Hm {}Heq /eval. rewrite (nth_map ord0) ?size_enum_ord //. have -> : to_word (ext_fun t) = [seq widen_ord (leqnSn n.+1) i | i <- to_word t]. by rewrite /ext_fun /to_word -map_rev map_flatten. case: i Hi => [i Hin] /= Hi. rewrite count_map; apply eq_count => /= [] [j Hj] /=. by apply/eqP/eqP => /(congr1 val) /= Heq; apply val_inj; rewrite /= Heq nth_enum_ord. + rewrite [RHS](tnth_nth 0) /= nth_rcons size_tuple. have:= Hi; rewrite ltnNge -ltnS => /negbTE ->; rewrite if_same. apply/count_memPn; rewrite {}Heq. apply/negP => /flattenP /= [rt2]. rewrite mem_rev /ext_fun => /mapP[/= rt _ ->{rt2}] /mapP[/= j _]. move=> /(congr1 val) /= Heq. move: Hi; rewrite Heq => /leq_ltn_trans/(_ (ltn_ord j)). by rewrite ltnn. - have mt2 i : i \in to_word t2 -> i < n.+1. apply contraLR; rewrite -leqNgt => Hi; apply/count_memPn. move: Hm; rewrite /eval => /(congr1 (fun t => tnth t i)). rewrite tnth_mktuple => ->. by rewrite [LHS](tnth_nth 0) /= nth_rcons size_tuple ltnNge Hi /= if_same. pose t : seq (seq 'I_n.+1) := [seq [seq inord (val i) | i <- r] | r <- t2]. have Ht : is_tab_of_shape la t. rewrite /is_tab_of_shape /=; apply/andP; split. + rewrite -incr_tab ?tabshP // => [] [i Hio] [j Hjo] /mt2 /= Hi /mt2 /= Hj. by rewrite !ltEord !inordK. + rewrite {}/t -(shape_tabsh t2) /shape /ext_fun -map_comp. by apply/eqP/eq_map => s; rewrite /= size_map. exists (TabSh Ht). + rewrite inE /= {Ht}/t. rewrite /eval; apply/eqP/eq_from_tnth => i; rewrite tnth_mktuple. rewrite /to_word -map_rev -map_flatten -/(to_word t2) count_map. have -> : tnth m i = tnth (rcons_tuple m 0) (widen_ord (leqnSn n.+1) i). by rewrite !(tnth_nth 0) nth_rcons /= size_tuple ltn_ord. move: Hm; rewrite /eval => /(congr1 (fun t => tnth t (widen_ord (leqnSn n.+1) i))) <-. rewrite tnth_mktuple; apply eq_in_count => j /= /mt2 Hj. apply/eqP/eqP => /(congr1 val) /=. * by rewrite inordK // => Heq; apply val_inj. * by move=> ->; apply val_inj; rewrite /= inordK. + apply val_inj => /=. apply (eq_from_nth (x0 := [::])); first by rewrite !size_map. move=> r Hr; rewrite (nth_map [::]); last by rewrite !size_map. apply (eq_from_nth (x0 := inh)). * by rewrite size_map -!nth_shape !shape_tabsh. * move=> c Hc. rewrite (nth_map inh); last by move: Hc; rewrite -!nth_shape !shape_tabsh. apply val_inj => /=. rewrite /t /= (nth_map [::]) // (nth_map inh) //. rewrite inordK //; apply: mt2. rewrite -/(get_tab _ (_, _)); apply: mem_to_word. by rewrite /in_shape nth_shape. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg ssrint fingroup perm) mathcomp(mpoly) tools combclass ordtype sorted partition tableau skewpart skewtab antisym Schur_mpoly freeSchur therule std stdtab unitriginv presentSn