proposition: Lemma trivIs u : trivIseq u -> trivIset [set i | i \in u].
proof: Proof. Proof using. rewrite /trivIseq => H; apply/trivIsetP => A B. rewrite !inE => HAin HBin. have:= HAin; have:= HBin; rewrite -!index_mem. rewrite -{2 3}(nth_index set0 HAin) -{2 3}(nth_index set0 HBin). set iA := index A u; set iB := index B u. wlog leqAB: iA iB / iA <= iB. move=> Hwlog HA HB; case (leqP iA iB) => HAB. - exact: (Hwlog iA iB HAB). - by rewrite eq_sym disjoint_sym; exact: (Hwlog iB iA (ltnW HAB)). move=> HiA HiB HAB. apply: H; rewrite HiA andbT ltn_neqAle leqAB andbT. by move: HAB; apply: contra => /eqP ->. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast