proposition: Lemma plact_map_in_incr : u =Pl v -> (map F u) =Pl (map F v).
proof: Proof. Proof using Hincr. move=> H. suff : {subset v <= u} /\ [seq F i | i <- u] =Pl [seq F i | i <- v] by move => []. move: v H; apply: gencongr_ind; first by split; last exact: plact_refl. move=> l v1 r v2 [Hperm Hu] Hrule. split. - move=> i; move/(_ i): Hperm. rewrite !mem_cat => Hperm /or3P[] H; apply: Hperm. + by rewrite H ?orbT. + have /allP := plactrule_homog v1 => /(_ _ Hrule)/perm_mem ->. by rewrite H ?orbT. + by rewrite H ?orbT. rewrite (plact_ltrans Hu) {Hu} !map_cat. apply: plact_catr; apply: plact_catl. apply: rule_gencongr => /=; move: Hrule => /plactruleP[]. - move/plact1P => [a] [b] [c] [Hord Hv1]; rewrite Hv1 => -> {v2}; subst v1. rewrite !mem_cat /=; move: Hord => /andP[]. move: Hperm => /subset_abc [Ha Hc Hb]. rewrite -(le_mono_in Hincr) // => -> /(Hincr Hb Hc) -> /=. by rewrite mem_seq1 eq_refl ?orbT. - move/plact1iP => [a] [b] [c] [Hord -> {v2} Hv1]; rewrite Hv1; subst v1. rewrite !mem_cat /=; move: Hord => /andP[]. move: Hperm => /subset_abc [Hc Ha Hb]. rewrite -(le_mono_in Hincr) // => -> /(Hincr Hb Hc) -> /=. by rewrite mem_seq1 eq_refl ?orbT. + move/plact2P => [a] [b] [c] [Hord Hv1]; rewrite Hv1 => -> {v2}; subst v1. rewrite !mem_cat /=; move: Hord => /andP[]. move: Hperm => /subset_abc [Hb Ha Hc]. move=> /(Hincr Ha Hb) ->; rewrite -(le_mono_in Hincr) // => ->. by rewrite mem_seq1 eq_refl ?orbT. + move/plact2iP => [a] [b] [c] [Hord -> {v2} Hv1]; rewrite Hv1; subst v1. rewrite !mem_cat /=; move: Hord => /andP[]. move: Hperm => /subset_abc [Hb Hc Ha]. move=> /(Hincr Ha Hb) ->; rewrite -(le_mono_in Hincr) // => ->. by rewrite mem_seq1 eq_refl ?orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr