proposition: Lemma subset_abc l a b c r : {subset l ++ [:: a; b; c] ++ r <= u} -> [/\ a \in u, b \in u & c \in u].
proof: Proof. Proof using. by move=> H; split; apply: H; rewrite !mem_cat !inE /= eq_refl !orbT. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) tools partition ordtype tableau stdtab Schensted congr