proposition: Lemma extract0 : extract set0 = [::].
proof: Proof. Proof using. rewrite /= extractIE /=. rewrite (eq_filter (a2 := pred0)); last by move=> i /=; rewrite in_set0. by rewrite filter_pred0. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype