proposition: Lemma append_nth_conj_tab (t : seq (seq T)) l i : is_part (shape t) -> is_add_corner (shape t) i -> conj_tab (append_nth t l i) = append_nth (conj_tab t) l (nth 0 (shape t) i).
proof: Proof. Proof using. move=> Hsh Hcorn; apply eq_from_shape_get_tab. - rewrite shape_conj_tab !shape_append_nth shape_conj_tab. exact: conj_part_incr_nth. - move=> [r c]; rewrite get_conj_tab; first last. by rewrite shape_append_nth; apply: is_part_incr_nth. rewrite !get_tab_append_nth. case: (r =P nth 0 (shape t) i); rewrite /= ?andbF ?andbT get_conj_tab // shape_conj_tab. move: Hcorn; rewrite /is_add_corner /= => /orP[/eqP Hi| H] Hr. + by rewrite Hi nth0 nth_default // size_conj_part. + have : nth 0 (shape t) i <= nth 0 (shape t) i < nth 0 (shape t) i.-1. by rewrite leqnn H. rewrite -nth_conjE //; last by case: i H {Hr}; rewrite // ltnn. by move=> /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau