proposition: Lemma sorted_sort_in T (P : {pred T}) (leT : rel T) : {in P & &, transitive leT} -> forall s : seq T, all P s -> sorted leT s -> sort leT s = s.
proof: Proof. move=> /in3_sig ? _ /all_sigP[s ->]. by rewrite sort_map sorted_map => /sorted_sort->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)