proposition: Lemma trivIsubseq u v : subseq u v -> trivIseq v -> trivIseq u.
proof: Proof. Proof using. elim: v u => [/= v1 /eqP -> //| v1 v IHv] u. case: u => [/= _ _ |u1 u /=]; first by move=> i j /= /andP[_]. case eqP => [->|_] Hsubs Htriv i j Hij. - move/(_ _ Hsubs (trivIseq_consK Htriv)): IHv => IHv. case: i Hij => [|i]; case: j => [// | j] /=; rewrite !ltnS; last exact: IHv. move/(mem_nth set0)/(mem_subseq Hsubs); set x := nth set0 u j => Hv. rewrite -(nth_index set0 Hv); move: Hv; rewrite -index_mem. move: (index x v) => i Hi. rewrite -[v1]/(nth set0 (v1 :: v) 0). rewrite -[nth set0 v i]/(nth set0 (v1 :: v) i.+1). exact: Htriv. - by apply: IHv => //; exact: (trivIseq_consK Htriv). Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast