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