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