proposition: Theorem invseqRSPQE s t : invseq s t -> (RStabmap s).1 = (RStabmap t).2.
proof: Proof. rewrite /RStabmap /= => Hinv. case HRSs : (RSmap s) => [Ps Qs] /=. have -> : Ps = RS s by rewrite -RSmapE HRSs. case HRSt : (RSmap t) => [Pt Qt] /=. have -> : Qt = (RSmap t).2 by rewrite HRSt. move Hn: (size s) => n {Ps Qs HRSs Pt Qt HRSt}. have Hsize := size_invseq Hinv. elim: n s t Hn Hinv Hsize => [/= | n IHn] s t Hn Hinv Hsize. by move: Hn Hsize => /eqP/nilP Hs; subst s => /= /esym/eqP/nilP -> /=. have:= shape_invseq Hinv. rewrite -!RSmapE [shape (RSmap t).1]shape_RSmap_eq !RSmapE. case Hs : s Hn Hinv Hsize => [// | s0 s']; rewrite -Hs => Hn Hinv Hsize. rewrite Hs (rembig_RS_last_big s0 s') shape_append_nth -Hs. set irow := last_big _ _. move=> Hshape. have Hszrem : size (rembig (s0 :: s')) = n. by move: Hn; rewrite Hs size_rembig /= => /succn_inj. case/lastP Ht : t => [// | t' tn]. by exfalso; move: Hsize; rewrite Hn Ht. have:= Hinv; rewrite Hs Ht => /invseqK Hrec. have Hsize' : size (rembig (s0 :: s')) = size (std t'). by rewrite size_rembig -Hs Hsize Ht size_rcons /std size_std_rec. move/(_ _ _ Hszrem Hrec Hsize'): IHn => IHn. move: Hshape; rewrite -Hs Ht /RSmap rev_rcons /= -/(RSmap t'). case HRSt : (RSmap t') => [t0 rowt']. case Hins : (instabnrow t0 tn) => [tr irowt'] /=. move: IHn; rewrite -Hs RSmap_std HRSt /= => ->. rewrite shape_stdtab_of_yam => /incr_nth_inj ->. congr (append_nth _ _ _). have:= (congr1 (fun t => sumn (shape t)) (RSmapE t')). rewrite (shape_RSmap_eq t') evalseq_eq_size HRSt => ->. rewrite -/(size_tab (RS t')) size_RS. move: Hsize; rewrite Ht Hn size_rcons => /succn_inj <-. move: Hinv => /invseq_is_std; rewrite Hs => /std_max ->. by apply succn_inj; rewrite -Hn Hs. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv