proposition: Lemma sort_stable_in T (P : {pred T}) (leT leT' : rel T) : {in P &, total leT} -> {in P & &, transitive leT'} -> forall s : seq T, all P s -> sorted leT' s -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s).
proof: Proof. move=> /in2_sig leT_total /in3_sig leT_tr _ /all_sigP[s ->]. by rewrite sort_map !sorted_map; apply: sort_stable. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)