proposition: Lemma homo_sort_map_in (T : Type) (T' : eqType) (P : {pred T}) (f : T -> T') leT leT' : {in P &, antisymmetric (relpre f leT')} -> {in P & &, transitive (relpre f leT')} -> {in P &, total leT} -> {in P &, {homo f : x y / leT x y >-> leT' x y}} -> forall s : seq T, all P s -> sort leT' [seq f x | x <- s] = [seq f x | x <- sort leT s].
proof: Proof. move=> /in2_sig leT'_asym /in3_sig leT'_trans /in2_sig leT_total. move=> /in2_sig f_homo _ /all_sigP[s ->]. rewrite [in RHS]sort_map -!map_comp /comp. by apply: homo_sort_map => // ? ? /leT'_asym /val_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)