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