proposition: Lemma is_part_incr_nthE sh i j : i.+1 < j -> is_part sh -> is_part (incr_nth (incr_nth sh j) i) -> is_part (incr_nth sh i) = is_part (incr_nth sh j).
proof: Proof. move=> Hij Hpart /is_partP[Hlastji Hpartij]. apply/idP/idP => /is_partP[H1 H2]; apply: (is_part_incr_nth Hpart) => /=. - case H : j => [//= | j'] /=; subst j. move/(_ j'): Hpartij; rewrite !nth_incr_nth. rewrite eq_refl (ltn_eqF (ltnW Hij)). rewrite ltnS in Hij; rewrite (ltn_eqF Hij) /=. by rewrite eq_sym ltn_eqF //= !add0n /= add1n. - case H : i => [//= | i'] /=; subst i. move/(_ i'): Hpartij; rewrite !nth_incr_nth. rewrite eq_refl (gtn_eqF (ltnW Hij)) (gtn_eqF (ltnW (ltnW Hij))). by rewrite eq_sym ltn_eqF //= !add0n /= add1n. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple finfun finset path bigop order) tools partition Yamanouchi ordtype std tableau stdtab Schensted congr plactic Greene_inv stdplact