proposition: Lemma index_leq_filter s (P : pred nat) i j : P i -> P j -> (index i (filter P s)) <= (index j (filter P s)) = (index i s <= index j s).
proof: Proof. Proof using . move=> Hi Hj. elim: s => //= s0 s IHs. case (boolP (P s0)) => [Hs0|] /=. - by case eqP; case eqP. - case eqP => [-> | _]; first by rewrite Hi. case eqP => [-> | _]; first by rewrite Hj. by rewrite ltnS 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