proposition: Lemma extractS (l : seq 'I_N) : sorted (fun i j : 'I_N => val i < val j) l -> extract [set i in l] = [seq tnth wt i | i <- l].
proof: Proof. Proof using. move=> HS; rewrite /= extractIE. congr ([seq tnth wt i | i <- _]). rewrite (eq_filter (a2 := mem l)); last by move => i; rewrite !inE. by rewrite mem_enum_seqE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype