proposition: Lemma append_nth_remn t : is_stdtab t -> t != [::] -> append_nth (remn t) (size_tab t).-1 (last_big t (size_tab t).-1) = t.
proof: Proof. by move=> H1 H2; have [] := remnP H1 H2. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau