proposition: Lemma gt_trans : transitive (@Order.gt _ Alph).
proof: Proof. by move=> x y z /= H1 H2; apply: (lt_trans H2 H1). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype