proposition: Lemma mem_shsh p u v : is_std u -> (p \in shsh u v) = ((sfiltergtn (size u) p == u) && (sfilterleq (size u) p == v)).
proof: Proof. move=> Hstdu; apply/idP/idP. - move=> H. by rewrite {2}(shsh_sfiltergtn Hstdu H) (shsh_sfilterleq Hstdu H) !eq_refl. - rewrite /shsh -(mem_shuffle _ (pred0_std v Hstdu)). move=> /andP[/eqP /= Hu /eqP /= Hv]. apply/and3P; split. + apply/eqP; rewrite -{2}Hu /=; apply: eq_filter => i. by rewrite /= (perm_mem Hstdu) mem_iota /= add0n. + apply/eqP; rewrite -{2}Hv sfilterleqK /=; apply: eq_in_filter => i /= Hi. by rewrite -Hv sfilterleqK mem_filter Hi andbT. + rewrite -(count_predC (gtn (size u)) p) -!size_filter. have /eq_filter -> : (predC (gtn (size u))) =1 leq (size u). by move=> i /=; rewrite -leqNgt. by rewrite Hu -Hv !size_map. 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