proposition: Lemma tnth_posc : tnth (in_tuple x) posc = c.
proof: Proof. Proof using a b u v. rewrite /x (tnth_nth c) nth_cat /=. have -> : (size u).+2 < size u = false. have:= leq_trans (leqnSn (size u)) (leqnSn _). by rewrite leqNgt => /negbTE ->. by rewrite -add1n addnS -addSn addnK. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene