proposition: Lemma enumUltV (U V : {set 'I_(size x)}) d : (forall l, l \in U -> l <= d) -> (forall l, l \in V -> l > d) -> enum (mem (U :|: V)) = enum U ++ enum V.
proof: Proof. Proof using. move => HU HV; rewrite /enum_mem /= -enumT /=. rewrite -{1}[enum 'I_(size x)](cat_take_drop d.+1) drop_enumI take_enumI filter_cat. congr (_ ++ _); rewrite -filter_predI; apply: eq_filter => i /=; rewrite !inE. - rewrite ltnS; case: (boolP (i \in U)) => HiU /=; first by rewrite HU. case: (boolP (i \in V)) => //= /(HV _). by rewrite ltnNge => /negbTE ->. - case: (boolP (i \in V)) => HiV /=; first by rewrite orbT HV. case: (boolP (i \in U)) => //= /(HU _). by rewrite ltnNge => ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools ordcast ordtype subseq partition tableau Yamanouchi stdtab Schensted congr plactic Greene