proposition: Lemma ksupp_inj_rev (leT : rel Alph) u k : ksupp_inj leT (fun y x => leT x y) k u (rev u).
proof: Proof. Proof using. case: u => [|u0 u] /=. exists set0; apply/and4P; split => /=. - by apply/eqP; congr (#|pred_of_set _|); apply/setP=> [][]/=. - by rewrite cards0. - by rewrite /trivIset /cover !big_set0 cards0. - by apply/forallP => s; rewrite inE /=. move: (u0 :: u) => {}u ks /and3P[Hsz Htriv /forallP Hall]. exists (cast_set (esym (size_rev u)) @: ((@revset _) @: ks)). apply/and4P; split. - rewrite cover_cast /cast_set /=. rewrite card_imset; last exact: cast_ord_inj. rewrite -size_cover_inj //; apply inv_inj; exact: rev_ordK. - apply: (@leq_trans #|ks|); last exact Hsz. rewrite -imset_comp; exact: leq_imset_card. - apply: imset_trivIset; first exact: cast_ord_inj. apply: imset_trivIset; last exact: Htriv. apply inv_inj; exact: rev_ordK. - apply/forallP => S1; apply/implyP => /imsetP[S2 /imsetP[S HS ->] -> {S1 S2}]. move/(_ S): Hall; rewrite HS /=. rewrite -(revK (extractpred (in_tuple (rev u)) _)) rev_sorted. rewrite !extractIE -map_rev -filter_rev. rewrite (eq_map (g := fun i => tnth (in_tuple u) (cast_ord (size_rev u) (rev_ord i)))); first last. move=> i /=. by rewrite !(tnth_nth u0) /= nth_rev ?{2}(size_rev u) // -(size_rev u). set S1 := (X in sorted _ X -> _); set S2 := (X in _ -> sorted _ X). suff -> : S1 = S2 by []. rewrite {}/S1 {}/S2 {k ks Hsz Htriv HS}. rewrite !map_comp; congr map; rewrite map_id. rewrite (eq_filter (a2 := fun i => cast_ord (size_rev u) (rev_ord i) \in S)); first last. rewrite /revset /cast_set => i /=. rewrite -{1}(cast_ordK (size_rev u) i). rewrite (mem_imset _ _ (cast_ord_inj (eq_n := _))) -{1}(rev_ordK i). have -> x : cast_ord (size_rev u) (rev_ord x) = rev_ord (cast_ord (size_rev u) x). by apply val_inj => /=; rewrite {1}size_rev. by rewrite (mem_imset _ _ rev_ord_inj). rewrite (map_filter_comp _ (fun i => _ i \in S) (@rev_ord _)). rewrite map_id -filter_map; congr filter. apply (inj_map val_inj); apply (eq_from_nth (x0 := 0)). by rewrite !size_map !size_rev size_map. rewrite size_map size_enum_ord => i Hi. rewrite -![X in _ = nth _ X _]map_comp. rewrite map_rev val_enum_ord (nth_iota _ _ Hi) add0n. rewrite nth_rev size_map size_enum_ord; last by rewrite size_rev. rewrite [X in X - _](size_rev). rewrite (eq_map (g := (fun i => (size u - i.+1)) \o val)); first last. by move=> j /=; rewrite {1}size_rev. rewrite map_comp val_enum_ord size_rev. have Hu : size u - i.+1 < size u by rewrite -subn_gt0 subKn. rewrite (nth_map 0); last by rewrite size_iota. rewrite (nth_iota _ _ Hu) add0n -(subSn Hi) subSS. by rewrite subKn; last exact: ltnW. Qed.
imports: mathcomp(all_ssreflect) mathcomp(perm) sorted tools subseq partition tableau Schensted congr plactic ordcast ordtype