proposition: Lemma sfilterleqK n v : shiftn n (sfilterleq n v) = [seq x <- v | n <= x].
proof: Proof. rewrite /=; elim: v => [// | v0 v IHv] /=. case: leqP => H /=; rewrite IHv; last by []. by rewrite subnKC. 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