proposition: Lemma size_append_nth t b i : size_tab (append_nth t b i) = (size_tab t).+1.
proof: Proof. Proof using. by rewrite /size_tab shape_append_nth sumn_incr_nth. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau