proposition: Lemma val2pos_inj : injective val2pos.
proof: Proof. Proof using. move: Hinvst => /linvseqP Hv. move=> i j; rewrite /val2pos; set posi := Ordinal _ => /(congr1 val) /= Heq. by apply/val_inj; rewrite /= -(Hv i (ltn_ord i)) -(Hv j (ltn_ord j)) Heq. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv