proposition: Lemma perm_append_nth t x pos : perm_eq (to_word (append_nth t x pos)) (x :: to_word t).
proof: Proof. Proof using. rewrite /append_nth; elim: t pos => [// | t0 t IHt] /=. - elim => [// | pos IHpos]. move: IHpos; rewrite /= to_word_cons cats0. by rewrite nth_default //= set_nth_nil. - case => [// | pos]. + rewrite !to_word_cons -cats1 -[x :: (_ ++ _)]cat1s. rewrite [flatten _ ++ _ ++ _]catA. by apply: permEl; apply: perm_catC. + move/(_ pos) : IHt; rewrite /= !to_word_cons. by rewrite -/((x :: to_word t) ++ t0) perm_cat2r. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau