proposition: Lemma sorted_extract_cond s P : sorted R (extract s) -> sorted R (extract (s :&: P)).
proof: Proof. Proof using HR. apply: subseq_sorted; first by move=> a b c /= H1 H2; apply: (HR H1 H2). by apply: extsubsI; rewrite -{2}[s]setIT; apply: setIS; exact: subsetT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype