proposition: Lemma get_tab_append_nth (t : seq (seq T)) l i r c : get_tab (append_nth t l i) (r, c) = if (r == i) && (c == nth 0 (shape t) i) then l else get_tab t (r, c).
proof: Proof. Proof using. rewrite /get_tab /append_nth nth_set_nth /=. case: (r =P i) => [-> | //] /=. rewrite nth_rcons nth_shape. case: (ltnP c (size (nth [::] t i))) => Hc; first by rewrite (ltn_eqF Hc). case: (c =P (size (nth [::] t i))) => // _. by rewrite nth_default. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau