proposition: Lemma size_cut_sizeu : size [seq i <- enum 'I_(size x) | val i < size u] = size u.
proof: Proof. Proof using l0 l1 v. suff -> : [seq i <- enum 'I_(size x) | val i < size u] = take (size u) (enum 'I_(size x)). rewrite size_take size_enum_ord size_cat. by rewrite addnS ltnS -{1}[size u]addn0 leq_add2l leq0n. apply: (inj_map val_inj); rewrite map_take val_enum_ord take_iota. rewrite (eq_filter (a2 := gtn ((size u))\o val)) //. by rewrite map_filter_comp /= val_enum_ord iotagtnk minnC map_id. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene