proposition: Lemma shsh_sfiltergtn p u v : is_std u -> p \in shsh u v -> u = sfiltergtn (size u) p.
proof: Proof. move=> Hstdu; rewrite /shsh. rewrite -(mem_shuffle _ (pred0_std v Hstdu)) => /and3P[/eqP Hu _ _]. rewrite -{1}Hu; apply: eq_filter => i /=. by rewrite (perm_mem Hstdu) mem_iota /= add0n. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype finfun fintype choice) mathcomp(order seq tuple finset perm binomial bigop) tools vectNK subseq partition Yamanouchi ordtype std tableau stdtab Schensted plactic Greene_inv stdplact