proposition: Lemma eq_Greene_rel (T : eqType) (R1 R2 : rel T) u : R1 =2 R2 -> Greene_rel R1 u =1 Greene_rel R2 u.
proof: Proof. exact: eq_Greene_rel_t. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype