proposition: Lemma trivIseq_shrows sh : trivIseq (shrows sh).
proof: Proof. Proof using. elim: sh => [/= | s0 sh /= IHsh]; first by rewrite /trivIseq => i j /= /andP[]. rewrite /trivIseq /= size_map => i j /andP[Hij Hj]. rewrite /disjoint; apply/pred0P => l /=; apply/negP => /andP[]. case: i j Hj Hij => [| i] [//= | j] /=; rewrite !ltnS => Hj. - move=> _ /imsetP[i Hi ->]. rewrite (nth_map set0 _ _ Hj) /shiftset /= imset_comp. rewrite mem_imset; last exact: cast_ord_inj. by move/imsetP => [j' _ /eqP]; rewrite eq_sym eq_lrshift. - move=> Hij; have Hi := ltn_trans Hij Hj. rewrite (nth_map set0 _ _ Hj) (nth_map set0 _ _ Hi) /shiftset /=. move=> /imsetP[k Hk ->]. rewrite mem_imset => Hk'; first last. exact: (inj_comp (@cast_ord_inj _ _ _) (@lshift_inj _ _)). have /IHsh : i < j < size (shrows sh) by rewrite Hij Hj. by rewrite /disjoint => /pred0P /(_ k); rewrite /= Hk Hk'. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype