proposition: Lemma extract2 i j : val i < val j -> extract [set i; j] = [:: tnth wt i; tnth wt j].
proof: Proof. Proof using. move=> Hij. have : sorted (fun i j : 'I_N => val i < val j) [:: i; j]. by rewrite /sorted /path Hij. move/extractS => /= <-; congr (extractpred wt (mem (pred_of_set _))). by apply/setP/subset_eqP/andP; split; apply/subsetP=> k; rewrite !inE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype