proposition: Lemma Greene_rel_t_uniq (leT : rel T) N (u : N.-tuple T) : uniq u -> Greene_rel_t leT u =1 Greene_rel_t (fun x y => (x != y) && (leT x y)) u.
proof: Proof. rewrite /Greene_rel_t => Huniq k. apply eq_bigl => S; rewrite /ksupp; congr [&& _, _ & _]. rewrite /=; apply eq_forallb_in => s _ {S k}. move: Huniq => /(subseq_uniq (extsubsm u (mem s))). case: (extractpred _ _) => {s} [| n s] //=. elim: s n => //= m s IHs n. by rewrite inE negb_or => /andP[/andP[-> _] /IHs ->]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype