proposition: Lemma Greene_rel_uniq (T : eqType) (leT : rel T) u : uniq u -> Greene_rel leT u =1 Greene_rel (fun x y => (x != y) && (leT x y)) u.
proof: Proof. by move=> Hu k; exact: Greene_rel_t_uniq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype