proposition: Lemma index_sfilterleq n s i : index i (sfilterleq n s) = index (i + n) (filter (leq n) s).
proof: Proof. Proof using . elim: s => //= s0 s IHs. case: (leqP n s0) => Hv0 /=. - by rewrite -{2}(subnK Hv0) eqn_add2r IHs. - by rewrite IHs. 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