proposition: Lemma shape_append_nth t b i : shape (append_nth t b i) = incr_nth (shape t) i.
proof: Proof. Proof using. rewrite /shape /=; apply: (@eq_from_nth _ 0). - rewrite size_map size_set_nth size_incr_nth size_map /maxn. by case: (ltngtP i.+1 (size t)). - move=> j Hi. rewrite nth_incr_nth (nth_map [::]) /=; last by move: Hi; rewrite size_map. rewrite nth_set_nth /= eq_sym. have -> : nth 0 [seq size i | i <- t] j = size (nth [::] t j). case: (ltnP j (size t)) => Hcase. + by rewrite (nth_map [::] _ _ Hcase). + by rewrite (nth_default _ Hcase) nth_default; last by rewrite size_map. case eqP => [->|]. + by rewrite size_rcons add1n. + by rewrite add0n. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau