proposition: Lemma homo_sort_map (T : Type) (T' : eqType) (f : T -> T') leT leT' : antisymmetric (relpre f leT') -> transitive (relpre f leT') -> total leT -> {homo f : x y / leT x y >-> leT' x y} -> forall s : seq T, sort leT' (map f s) = map f (sort leT s).
proof: Proof. move=> leT'_asym leT'_trans leT_total f_homo s; case Ds: s => // [x s']. rewrite -{}Ds -(mkseq_nth x s) [in RHS]sort_map -!map_comp /comp. apply: (@sorted_eq_in _ leT') => [? ? ?|? ?|||]; rewrite ?mem_sort. - by move=> /mapP[? _ ->] /mapP[? _ ->] /mapP[? _ ->]; apply/leT'_trans. - by move=> /mapP[? _ ->] /mapP[? _ ->] /leT'_asym ->. - apply: (sort_sorted_in _ (allss _)) => _ _ /mapP[y _ ->] /mapP[z _ ->]. by case/orP: (leT_total (nth x s y) (nth x s z)) => /f_homo ->; rewrite ?orbT. - by rewrite map_comp -sort_map; exact/homo_sorted/sort_sorted. - by rewrite perm_sort perm_map // perm_sym perm_sort. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)