proposition: Lemma trivIseq_consK u0 u : trivIseq (u0 :: u) -> trivIseq u.
proof: Proof. Proof using. by rewrite /trivIseq => H i j Hij; apply: (H i.+1 j.+1); rewrite /= !ltnS. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast