proposition: Lemma unlift_seqE n (l : seq 'I_n.+1) : sorted (fun i j : 'I_n.+1 => i < j) (ord0 :: l) -> exists l1 : seq 'I_n, sorted (fun i j : 'I_n => i < j) l1 /\ l = map (lift ord0) l1.
proof: Proof. elim: l => [_ | l0 l IHl] /=. - by exists [::] => /=; split. - move=> /andP[H0 Hl]. have: sorted (fun i j : 'I_n.+1 => i < j) (ord0 :: l). rewrite /sorted; move: l Hl {IHl}; case => [// | l1 l] /= /andP[Hl1 ->]. by rewrite (ltn_trans H0 Hl1). move/IHl => {IHl} [r] [Hr Heq]; rewrite Heq. case: l0 H0 Hl => [[// | r0 /= Hr0 _]] Hl. have:= Hr0; rewrite ltnS => Hr0'. exists ((Ordinal Hr0') :: r); split. + move: Hr; rewrite /sorted; case: r Heq => [// | r1 r] /= Heq. case: r1 Heq => r1 Hr1 /= Heq. move: Hl; rewrite Heq /= => /andP[]. by rewrite /fintype.bump leq0n /= add1n ltnS => -> /=. + by rewrite /=; congr (_ :: _); exact: val_inj. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast