proposition: Lemma rcast_com : (cast_ord (esym (size_to_word (t0 :: t)))) \o sym_cast \o (@rshift (sumn (shape t)) (size t0)) =1 rsh_rec.
proof: Proof. Proof using. by move=> i; apply/eqP; rewrite /rsh_rec /eq_op /= size_to_word. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype