proposition: Lemma enum_cut : enum 'I_(size x) = [seq i <- enum 'I_(size x) | val i < size u] ++ [:: pos0; pos1] ++ [seq i <- enum 'I_(size x) | val i >= (size u) + 2].
proof: Proof. Proof using. rewrite [RHS]catA -{1}[enum 'I_(size x)](cat_take_drop ((size u) + 2)). rewrite -drop_enumI; congr (_ ++ _). rewrite take_enumI -{1}[enum 'I_(size x)](cat_take_drop (size u)). rewrite filter_cat //=; congr (_ ++ _). - rewrite take_enumI -filter_predI. apply eq_filter=> i /=; apply: andb_idl => /ltn_trans; apply. by rewrite -{1}[size u](addn0); rewrite ltn_add2l. - apply: (inj_map val_inj) => /=. rewrite map_filter_comp map_drop val_enum_ord drop_iota add0n /x !size_cat. rewrite addKn !iotaD map_id filter_cat -[RHS]cats0. congr (_ ++ _). + by rewrite /= !addnS addn0 ltnSn (ltn_trans (ltnSn _) (ltnSn _)). + rewrite (eq_in_filter (a2 := pred0)); first by rewrite filter_pred0. by move=> i; rewrite mem_iota /= leqNgt => /andP[/negbTE ->]. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene