proposition: Lemma is_yam_plactic y : is_yam y -> forall w, y =Pl w -> is_yam w.
proof: Proof. move=> Hy; apply: gencongr_ind; first exact Hy. elim=> [/= | a0 aw /= IHaw]. - move=> b1 cw b2 H /plactruleP[] Hrew. + move: Hrew H => /plact1P[a] [b] [c] []. rewrite leEnat ltEnat /= => /andP[Hab Hbc] -> -> /=. set yc := (incr_nth (evalseq cw) b). move=> /and4P[H1 H2 Hpart ->]; rewrite Hpart. rewrite incr_nthC H1 !andbT /=. case (ltnP a.+1 c) => Hac; first by rewrite (is_part_incr_nthE Hac). have {}Hab : a = b. apply/eqP; rewrite eqn_leq Hab /= -ltnS. exact: (leq_trans Hbc). subst a. have {Hac}Hbc : c = b.+1 by apply/eqP; rewrite eqn_leq Hbc Hac. subst c. by rewrite -is_part_incr_nth1E. + move: Hrew H => /plact1iP[a] [b] [c] []. rewrite leEnat ltEnat /= => /andP[Hab Hbc] -> -> /=. set yc := (incr_nth (evalseq cw) b). move=> /and4P[]; rewrite incr_nthC => H1 H2 Hpart Hyam. rewrite Hpart Hyam H1 !andbT /=. case (ltnP a.+1 c) => Hac; first by rewrite -(is_part_incr_nthE Hac Hpart). have {}Hab : a = b. apply/eqP; rewrite eqn_leq Hab /= -ltnS. exact: (leq_trans Hbc). subst a. have {Hac}Hbc : c = b.+1 by apply/eqP; rewrite eqn_leq Hbc Hac. subst c; subst yc. rewrite incr_nthC is_part_incr_nth1E; first exact Hpart. exact: is_part_eval_yam. + move: Hrew H => /plact2P[a] [b] [c] []. rewrite leEnat ltEnat /= => /andP[Hab Hbc] -> -> /=. move=> /and4P[]; rewrite [(incr_nth (incr_nth _ a) c)]incr_nthC. move => H1 H2 Hpart Hyam. rewrite Hyam H1 H2 !andbT /= {H1}. case (ltnP a.+1 c) => Hac. by rewrite (is_part_incr_nthE Hac (is_part_eval_yam Hyam)). have {}Hbc : b = c. by apply/eqP; rewrite eqn_leq Hbc /=; exact: (leq_trans Hac). subst b. have {Hab}Hac : c = a.+1 by apply/eqP; rewrite eqn_leq Hac Hab. subst c. by rewrite -(is_part_incr_nth1E _ (is_part_eval_yam Hyam)). + move: Hrew H => /plact2iP[a] [b] [c] []. rewrite leEnat ltEnat /= => /andP[Hab Hbc] -> -> /=. move=> /and4P[]; rewrite (incr_nthC _ a c) => H1 H2 Hpart Hyam. rewrite Hyam H1 H2 !andbT /=. case (ltnP a.+1 c) => Hac. by rewrite -(is_part_incr_nthE Hac (is_part_eval_yam Hyam)). have {}Hbc : b = c. by apply/eqP; rewrite eqn_leq Hbc /=; exact: (leq_trans Hac). subst b. have {Hab}Hac : c = a.+1 by apply/eqP; rewrite eqn_leq Hac Hab. subst c. apply (is_part_incr_nth (is_part_eval_yam Hyam)) => /=. move: H1 => /is_partP[_ /(_ a)]. by rewrite !nth_incr_nth !eq_refl [_.+1 == _]eq_sym ltn_eqF. - move=> b1 cw b2 /andP[Hpart Hyam] Hrew. rewrite (IHaw _ _ _ Hyam Hrew) andbT. suff -> : (evalseq (aw ++ b2 ++ cw)) = (evalseq (aw ++ b1 ++ cw)) by []. rewrite -!evalseq_countE /evalseq_count /=. have Hperm : perm_eq (aw ++ b1 ++ cw) (aw ++ b2 ++ cw). apply: plact_homog; apply: plact_is_congr; apply: rule_gencongr; exact Hrew. rewrite !foldr_maxn (perm_big _ Hperm) /=. apply eq_map => i /=. by move: Hperm => /permP ->. 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