proposition: Lemma size_extract s : size (extract s) = #|s|.
proof: Proof. Proof using. by rewrite /extractpred size_map cardE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype