proposition: Lemma invseqK s0 s t tn : invseq (s0 :: s) (rcons t tn) -> invseq (rembig (s0 :: s)) (std t).
proof: Proof. move=> Hinv; apply: linvseq_sizeP; first exact: (linvseqK Hinv). rewrite size_rembig /= size_std. by move: Hinv => /size_invseq; rewrite size_rcons /= => /succn_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