proposition: Lemma rshift_recP : injective rsh_rec.
proof: Proof. Proof using. by move=> [i Hi] [j Hj] /eqP H; apply/eqP; move: H; rewrite !/eq_op /= eqn_add2l. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype