proposition: Lemma Greene_rel_t_cast R M N (Heq : M = N) k (V : M.-tuple T) : Greene_rel_t R (tcast Heq V) k = Greene_rel_t R V k.
proof: Proof. by subst M. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype