proposition: Lemma shrows_cards sh : map (fun S : {set 'I_(sumn sh)} => #|S|) (shrows sh) = sh.
proof: Proof. Proof using. elim: sh => [// | s0 sh IHsh] /=. rewrite imset_comp card_imset; last exact: cast_ord_inj. rewrite card_imset; last exact: rshift_inj. rewrite card_ord; congr (_ :: _). rewrite -map_comp -{}[RHS]IHsh; apply: eq_map. move=> S /=; rewrite imset_comp. rewrite card_imset; last exact: cast_ord_inj. by rewrite card_imset; last exact: lshift_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype