proposition: Lemma shsh_sfilterleq p u v : is_std u -> p \in shsh u v -> v = sfilterleq (size u) p.
proof: Proof. move=> Hstdu; rewrite /shsh => Hsh. rewrite sfilterleqE; have:= Hsh. rewrite -(mem_shuffle _ (pred0_std v Hstdu)) /= => /and3P[_ /eqP <- _]. apply: eq_in_filter => i /= Hi. have /allP/(_ p Hsh) Hp := perm_shuffle u (shiftn (size u) v). move: Hi; rewrite -(perm_mem Hp) mem_cat => /orP[]. - rewrite (perm_mem Hstdu) mem_iota /= add0n /shiftn => Hi. rewrite leqNgt Hi /=; apply/negP => /mapP[j Hj Heq]. by move: Hi; rewrite Heq -{2}[size u]addn0 ltn_add2l. - move=> Hi; rewrite Hi; apply: esym. move: Hi; rewrite /shiftn => /mapP[j _ ->]. by rewrite -{1}[size u]addn0 leq_add2l. 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