proposition: Lemma bigcup_seq_cover (u : seq {set T}) : \bigcup_(s <- u) s = cover [set s in u].
proof: Proof. Proof using. by rewrite bigcup_seq; apply: eq_bigl => i; rewrite inE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast