proposition: Lemma extsubsIm n wt (P1 P2 : pred 'I_n) : subpred P1 P2 -> subseq (extractpred wt P1) (extractpred wt P2).
proof: Proof. Proof using. rewrite !extractmaskE; case: wt => w /= _. elim: n w P1 P2 => [// | n IHn] w P1 P2 H; first by rewrite enum0. case: w => [// | w0 w]; first by rewrite !mask0. rewrite enum_ordSl /= -map_comp -map_comp. case (boolP (P1 ord0)) => H1. - by rewrite (H ord0 H1) /= eq_refl; apply: IHn => i /=; apply: H. - case (boolP (P2 ord0)) => H2. rewrite -cat1s. set ss := (X in subseq _ (_ ++ X)). apply: (@subseq_trans _ ([::] ++ ss)); last exact: suffix_subseq. by rewrite cat0s /ss {ss}; apply: IHn => i /=; apply: H. by apply: IHn => i /=; apply: H. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype