proposition: Lemma set_nth_LxR L c R l pos : (size L) = pos -> set_nth l (L ++ c :: R) pos l = L ++ l :: R.
proof: Proof. Proof using. move Hr : (L ++ c :: R) => r Hsize. have Hpos : pos < size r by rewrite -Hsize -Hr size_cat /= -addSnnS -{1}[(size L).+1]addn0 leq_add2l. have Hsizeset : size (set_nth l r pos l) = size r. rewrite size_set_nth maxnC /maxn ltnS. by move: Hpos; rewrite ltnNge => /negbTE => ->. apply: (eq_from_nth (x0 := l)) => [| i]. - rewrite (_ : size (_ ++ _ :: _) = size r); last by rewrite -Hr !size_cat. by rewrite Hsizeset. - rewrite Hsizeset nth_set_nth -/pos nth_cat Hsize /= => Hi. case (ltngtP i pos) => Hipos. + by rewrite -Hr nth_cat Hsize Hipos. + rewrite -Hr nth_cat Hsize. have:= ltnW Hipos; rewrite leqNgt => /negbTE ->. case H : (i - pos) => [|//=]. exfalso; have H1 : i <= pos by rewrite /leq H. by have:= leq_trans Hipos H1; rewrite ltnn. + by rewrite Hipos subnn. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr