fact: Definition trivIseq (u : seq {set T}) : Prop := forall i j, i < j < size u -> [disjoint (nth set0 u i) & (nth set0 u j)].
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast