proposition: Lemma tnth_pos0 : tnth (in_tuple x) pos0 = l0.
proof: Proof. Proof using. by rewrite (tnth_nth l0) nth_cat (_ : pos0 < size u = false) ?ltnn // subnn. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene