proposition: Lemma posbig_invseq s0 s t tn : invseq (s0 :: s) (rcons t tn) -> posbig (s0 :: s) = tn.
proof: Proof. move => Hinv; have:= Hinv; rewrite /invseq => /andP[Hst Hts]. have Hpos := posbig_size_cons s0 s. have Hszt : size t < size (rcons t tn) by rewrite size_rcons. have:= linvseq_ltn_szt Hts Hszt. rewrite nth_rcons ltnn eq_refl (size_invseq Hinv) => Htn. have:= invseq_nthE Hinv Hpos Hszt. rewrite (set_nth_default inh _ Hpos) nth_posbig. rewrite nth_rcons ltnn eq_refl => ->. rewrite (std_max (invseq_is_std Hinv)); apply/eqP. by move: Hinv => /size_invseq; rewrite size_rcons /= => /eqP. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv