proposition: Lemma is_tab_append_nth_size_alternative_proof r T n : all (gtn n) (to_word T) -> is_part (incr_nth (shape T) r) -> is_tableau T -> is_tableau (append_nth T n r).
proof: Proof. have get_append_nth_in rc : in_shape (shape T) rc -> get_tab (append_nth T n r) rc = get_tab T rc. move: rc => [rn c]. rewrite /get_tab /append_nth nth_set_nth /=. case: (rn =P r) => // ->{rn} /in_shape_tab. by rewrite nth_rcons => ->. have get_append_nth_eq : get_tab (append_nth T n r) (r, nth 0 (shape T) r) = n. rewrite nth_shape /get_tab /append_nth nth_set_nth /= eq_refl /=. by rewrite nth_rcons eq_refl ltnn. move=> /allP Hw Hparti /is_tableau_getP[Hpart Hrow Hcol]. apply/is_tableau_getP; split => [| rn c Hini | rn c Hini]. - by rewrite shape_append_nth. - case: (boolP (in_shape (shape T) (rn, c.+1))) => Hin. + rewrite !get_append_nth_in //; first exact: Hrow. by apply (in_part_le Hpart Hin). + move: Hini Hin {Hcol Hpart Hparti}; rewrite /in_shape. rewrite shape_append_nth nth_incr_nth /=. case eqP => [<-{rn} /= | _]; last by rewrite add0n => ->. rewrite add1n ltnS -leqNgt => H1 H2. have {H1 H2} H : c.+1 = nth 0 (shape T) r. by apply anti_leq; rewrite H1 H2. rewrite H get_append_nth_eq get_append_nth_in ?/in_shape ?H //. rewrite leEnat; apply/ltnW/Hw. by apply mem_to_word; rewrite /in_shape H. - case: (boolP (in_shape (shape T) (rn.+1, c))) => Hin. + rewrite !get_append_nth_in //; first exact: Hcol. by apply (in_part_le Hpart Hin). + move: Hini Hin {Hcol Hrow}; rewrite /in_shape. rewrite shape_append_nth nth_incr_nth. case eqP => [/= Hrn | _]; last by rewrite add0n => ->. rewrite -Hrn add1n ltnS -leqNgt => H1 H2. have {H1 H2} H : c = nth 0 (shape T) r. by apply anti_leq; rewrite H1 H2. have {Hpart Hparti} Hshape : nth 0 (shape T) r < nth 0 (shape T) rn. move: Hparti => /is_partP => [] [_] /(_ rn). by rewrite !nth_incr_nth {}Hrn eq_refl add1n eq_sym ltn_eqF. rewrite H get_append_nth_eq get_append_nth_in ?/in_shape ?H //. rewrite ltEnat; apply Hw. by apply mem_to_word; rewrite /in_shape. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass partition Yamanouchi ordtype std tableau