proposition: Lemma shcol_cards sh : is_part sh -> map (fun S : {set 'I_(sumn sh)} => #|S|) (shcols sh) = conj_part sh.
proof: Proof. Proof using. elim: sh => [// | s0 sh IHsh] /= /andP[Hhead Hpart]. rewrite -map_comp. rewrite (eq_map (g := fun i : 'I_(_) => (nth 0 (conj_part sh) i).+1)); first last. move=> i; rewrite /= cardsU. rewrite cards1 imset_comp card_imset; last exact: cast_ord_inj. rewrite card_imset; last exact: lshift_inj. rewrite add1n -(IHsh Hpart). rewrite [X in _ - #|pred_of_set X|](_ : _ = set0); first last. apply/setP => j; rewrite !inE. apply/negP => /andP[/eqP -> {j}]. rewrite mem_imset; last exact: cast_ord_inj. by move/imsetP => [j _ /eqP]; rewrite eq_sym eq_lrshift. rewrite cards0 subn0. case (ltnP i (size (shcols sh))) => Hi. - by rewrite (nth_map set0 _ _ Hi). - rewrite (nth_default _ Hi) nth_default; last by rewrite size_map. by rewrite cards0. elim: sh s0 Hhead Hpart {IHsh} => [//= | s1 sh IHsh] /=. - move=> s0 Hs0 _; apply: (@eq_from_nth _ 0). + by rewrite size_map size_nseq size_enum_ord. + move=> i; rewrite size_map size_enum_ord => Hi. rewrite nth_nseq Hi (nth_map (Ordinal Hs0)); last by rewrite size_enum_ord. by rewrite nth_nil. - move=> s0 Hs1 /andP[Hhead Hpart]. rewrite -(IHsh s1 Hhead Hpart) {IHsh}. move HS : (map _ (enum 'I_s1)) => S. have : size S <= s0 by rewrite -HS size_map size_enum_ord. elim: S {HS s1 Hhead Hpart sh Hs1} s0 => [// s0 _| l0 l IHl] /=. + apply: (@eq_from_nth _ 0); first by rewrite size_map size_nseq size_enum_ord. move=> i; rewrite size_map size_enum_ord => Hi. rewrite nth_nseq Hi (nth_map (Ordinal Hi)); last by rewrite size_enum_ord. by rewrite nth_nil. + case => [// | s0]; rewrite ltnS => /IHl <- {IHl}. rewrite (eq_map (g := (fun i => (nth 0 (l0 :: l) i).+1) \o val)) //. rewrite map_comp val_enum_ord /=. rewrite -[1]addn0 iotaDl -map_comp. pose f := fun i => (nth 0 l i).+1. rewrite (eq_map (g := f)) //; apply esym. rewrite (eq_map (g := f \o nat_of_ord)) //. by rewrite [map _ (enum _)]map_comp val_enum_ord /=. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype