proposition: Theorem RSmap_std (d : unit) (T : inhOrderType d) (w : seq T) : (RSmap (std w)).2 = (RSmap w).2.
proof: Proof. move Hn : (size w) => n. elim: n d T w Hn => [/= | n IHn] d T w; first by move/eqP/nilP => ->. case/lastP Hw : w => [// | w' wn] Hn. have:= shape_RS_std (rcons w' wn). rewrite -!RSmapE !shape_RSmap_eq. case/lastP H : (std (rcons w' wn)) => [/= | st stn]. exfalso; move: H => /(congr1 size). by rewrite size_std_rec size_rcons. case HRS : ((RSmap (rcons w' wn)).2) => [/= | iw yamw]. exfalso; move: HRS => /(congr1 size). by rewrite size_RSmap2 size_rcons. have Hyamw : yamw = (RSmap w').2. move: HRS; rewrite /RSmap rev_rcons /=. case: (RSmap_rev (rev w')) => [t rows] /=. by case: (instabnrow t wn) => [tr nrow] /= [_ ->]. have Hsize : size w' = n by move: Hn; rewrite size_rcons => /succn_inj. have /std_rconsK Hst : std (rcons w' wn) = std (rcons st stn). by rewrite -H std_stdE. rewrite {wn Hw Hn H HRS} Hyamw /= -(IHn _ _ _ Hsize). have Hsizest : size st = n. move: Hst; rewrite /std -{2}(size_std_rec (size st) st) => <-. by rewrite size_std_rec. rewrite Hst (IHn _ _ _ Hsizest) {Hst IHn Hsize Hsizest}. rewrite /RSmap rev_rcons /= -[RSmap_rev (rev st)]/(RSmap st). case HRS : (RSmap st) => [t0 rows]. by case Hins : (instabnrow t0 stn) => [tr irow] /= /incr_nth_inj ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv