proposition: Lemma mem_enum_seqE n (l : seq 'I_n) : sorted (fun i j : 'I_n => val i < val j) l -> [seq i <- enum 'I_n | i \in l] = l.
proof: Proof. elim: n l => [|n IHn] [| l0 l]. - rewrite (eq_filter (a2 := pred0)); first by rewrite filter_pred0. by move=> i /=; rewrite in_nil. - by move=> _; have:= ltn_ord l0; rewrite ltn0. - rewrite (eq_filter (a2 := pred0)); first by rewrite filter_pred0. by move=> i /=; rewrite in_nil. - rewrite (enum_ordSl n) /=. case: l0 => [[/=| l0] Hl0]. + have -> : Ordinal Hl0 = ord0 by exact: val_inj. move/unlift_seqE => [l1] [{}/IHn <- Hl]. rewrite {2}Hl; congr (_ :: _). rewrite filter_map (eq_in_filter (a2 := fun i => i \in l1)) //=. move=> i _ /=; rewrite Hl in_cons. have:= neq_lift ord0 i; rewrite eq_sym => /negbTE -> /=. rewrite mem_map; last exact: lift_inj. apply/idP/idP; first by rewrite mem_filter => /andP[]. by move=> Hi; rewrite mem_filter Hi /= mem_enum inE. + move=> Hpath; have H0 : @ord0 n.+1 < Ordinal Hl0 by []. have: sorted (fun i j : 'I_n.+1 => i < j) (ord0 :: Ordinal Hl0 :: l) by []. move/unlift_seqE => [l1] [Hsort1 ->]. rewrite ord0_in_map_liftF -(IHn l1 Hsort1) filter_map /=. rewrite (eq_filter (a2 := mem l1)) // => i /=. rewrite mem_map; last exact: lift_inj. apply/idP/idP; first by rewrite mem_filter => /andP[]. by move=> /= Hi; rewrite mem_filter Hi /= mem_enum inE. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast