proposition: Lemma trivIseq_shcols sh : trivIseq (shcols sh).
proof: Proof. Proof using. elim: sh => [/= | s0 sh /= IHsh]; first by rewrite /trivIseq => i j /= /andP[]. rewrite /trivIseq size_shcols_cons => i j /andP[Hij Hj]. have Hi := ltn_trans Hij Hj. rewrite /disjoint; apply/pred0P => l /=; apply/negP => /andP[]. rewrite [nth _ _ i](nth_map (Ordinal Hi)); last by rewrite size_enum_ord. rewrite [nth _ _ j](nth_map (Ordinal Hj)); last by rewrite size_enum_ord. rewrite !nth_enum_ord //=. rewrite in_setU1 => /orP[]. - move/eqP => ->; rewrite in_setU1 => /orP[]; rewrite /sym_cast /=. + by rewrite /eq_op /= !nth_enum_ord //= eqn_add2l (ltn_eqF Hij). + move/imsetP => [k _ /= /cast_ord_inj /eqP]. by rewrite eq_sym eq_lrshift. - move/imsetP => [li Hli -> {l}]. rewrite in_setU1 => /orP[]. + by rewrite /= (inj_eq (cast_ord_inj (eq_n:=_))) eq_lrshift. + move/imsetP => [l Hlj /= /cast_ord_inj /lshift_inj H]; move: H Hli => -> Hli. case: (ltnP j (size (shcols sh))) => Hj1; last by move: Hlj; rewrite (nth_default _ Hj1) in_set0. have : i < j < size (shcols sh) by rewrite Hij Hj1. move/(IHsh i j); rewrite /disjoint => /pred0P/(_ l). by rewrite /= Hli Hlj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype