proposition: Lemma is_part_incr_nth1E sh i : is_part sh -> is_part (incr_nth (incr_nth sh i.+1) i) = is_part (incr_nth sh i).
proof: Proof. move=> Hpart; apply/idP/idP => Hparti. - apply (is_part_incr_nth Hpart) => /=. case: i Hparti => [//= | i] /is_partP[_ Hparti /=]. move/(_ i): Hparti. rewrite !nth_incr_nth /= eq_refl. rewrite eq_sym ltn_eqF // eq_sym ltn_eqF //. have -> /= : (i.+2 == i) = false by elim i. by rewrite !add0n /= add1n. - rewrite incr_nthC; apply (is_part_incr_nth Hparti) => /=. elim: sh i Hpart Hparti => [//= | s0 sh IHsh] /= i. by move=> _ /part_head_non0 Hhead; have -> : i = 0 by case: i Hhead. case: i => [| i] /= /andP[Head Hp]; first by move=> _ ; move: Head; case sh. by move=> /andP[_ Hpi]; exact: IHsh. 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