proposition: Lemma plact2i_homog : forall u : word, all (perm_eq u) (plact2i u).
proof: Proof. Proof using. move=> u; apply/allP => v /plact2iP. move=> [a] [b] [c] [/andP[H1 H2] -> ->] /=; rewrite /perm_eq /=. rewrite !eq_refl ![c == a]eq_sym ![c == b]eq_sym ![b == a]eq_sym /=. by case Hab : (b == c); rewrite (lt_eqF H1) (lt_eqF (lt_le_trans H1 H2)) !eq_refl /=. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr