proposition: Lemma sorted_std_extract u (S : {set 'I_(size u)}) : sorted <=%O (extractpred (in_tuple u) (mem S)) = sorted <=%O (extractpred (in_tuple (std u)) (mem (cast_set (esym (size_std u)) S))).
proof: Proof. Proof using. rewrite /extractpred cast_enum /= /sorted. set leqI := (fun i j : 'I_(size u) => i <= j). have leqI_trans : transitive leqI. move=> i j k; rewrite /leqI; exact: leq_trans. have: sorted leqI (enum (mem S)). rewrite {1}/enum_mem -enumT /=. apply: (sorted_filter leqI_trans). exact: enum_ord_sorted. case: (enum (mem S)) => [// | i0 l] {S} /=. elim: l i0 => [// | i1 l IHl] i0 /= /andP[Hleqi Hpath]. rewrite -(IHl i1 Hpath) {IHl Hpath}; congr (_ && _). rewrite !(tnth_nth inh) /=. have:= eq_inv_std u => /eq_invP[Hsz]; apply. move: Hleqi; rewrite /leqI => -> /=. exact: ltn_ord. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm fingroup) tools combclass ordcast partition Yamanouchi ordtype std tableau stdtab sorted Schensted congr plactic Greene Greene_inv