proposition: Lemma size_RSmapinv2_yam d (disp : unit) (Typ : inhOrderType disp) (tab : seq (seq Typ)) (T : stdtabn d) : size (RSmapinv2 (tab, yam_of_stdtab T)) = d.
proof: Proof. Proof using . rewrite -{2}(size_tab_stdtabn T) -size_yam_of_stdtab // /RSmapinv2 /=. elim: (yam_of_stdtab _) tab => [//= | w0 w /= IHw] tab. case: (invinstabnrow _ _) => [tr lr]. by rewrite size_rcons IHw. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(ssralg) mathcomp(ssrcomplements freeg mpoly) tools ordtype partition Yamanouchi std tableau stdtab Schensted congr plactic stdplact Yam_plact Greene_inv shuffle Schur_mpoly