proposition: Lemma eq_Greene_rel_t (R1 R2 : rel T) N (u : N.-tuple T) : R1 =2 R2 -> Greene_rel_t R1 u =1 Greene_rel_t R2 u.
proof: Proof. rewrite /Greene_rel_t /= => H k. apply eq_bigl => S; rewrite /ksupp; congr [&& _, _ & _]. rewrite /=; apply eq_forallb_in => s _. case: (extractpred _ _) => [| e t] //=. by rewrite (eq_path H). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype