proposition: Lemma is_stdtab_remn t : is_stdtab t -> is_stdtab (remn t).
proof: Proof. move Hn : (size_tab t) => n. case: n Hn => [| n]; first by move=> /tab0 H /andP[/H ->]. move=> Hsize Hstdtab. case: (t =P [::]) => [-> // | /eqP/(remnP Hstdtab)]. rewrite Hsize /= => [] [Htab Happ]. move: Hstdtab; rewrite /is_stdtab Htab /= /is_std. rewrite !size_to_word {1}Hsize => /andP[_ Hperm]. have/(congr1 size_tab) := Happ. rewrite size_append_nth Hsize => /eqP; rewrite eqSS => /eqP Hsz. have:= perm_append_nth (remn t) n (last_big t n). rewrite {}Happ Hsz (permPl Hperm) perm_sym. rewrite -(addn1 n) iotaD /= add0n cats1. by rewrite perm_sym perm_rcons perm_sym perm_cons. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau