proposition: Lemma tnth_pos1 : tnth (in_tuple x) pos1 = l1.
proof: Proof. Proof using. rewrite (tnth_nth l1) nth_cat. have -> : pos1 < size u = false. by have:= leqnSn (size u); rewrite leqNgt => /negbTE ->. by rewrite subSn //= subnn. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene