proposition: Lemma find_append_nth (l : nat) t r : l \notin (to_word t) -> find (fun x : seq nat => l \in x) (append_nth t l r) = r.
proof: Proof. rewrite /append_nth. elim: r t => [/= | r IHr] t /=; case: t => [_ | t0 t] /=. - by rewrite inE eq_refl. - by rewrite mem_rcons inE eq_refl. - apply/eqP; rewrite eqSS. elim: r {IHr} => [/= | r]; first by rewrite inE eq_refl. by rewrite /ncons /= => /eqP ->. - by rewrite to_word_cons mem_cat negb_or => /andP[{}/IHr-> /negbTE->]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau