proposition: Lemma nth_inspos_ins : nth l ins pos = l.
proof: Proof. Proof using. by rewrite /ins nth_set_nth /= eq_refl. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools partition Yamanouchi ordtype subseq tableau std stdtab