proposition: Lemma auxbijP p (y : yameval p) : is_yam_of_eval p ((RSmap y).2).
proof: Proof. rewrite /is_yam_of_eval is_yam_RSmap2 /=. rewrite -shape_RSmap_eq RSmapE. by rewrite (shape_RS_yam (yamevalP y)) eval_yameval. 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