proposition: Lemma sort_sorted_in_lt (s : seq A) ltT : irreflexive ltT -> antisymmetric ltT -> transitive ltT -> uniq s -> {in s &, total (fun k t => (k == t) || ltT k t)} -> sorted ltT (sort (fun k t => (k == t) || ltT k t) s).
proof: Proof. move=>I S T U Tot; rewrite lt_sorted_uniq_le //. by rewrite sort_uniq U (sort_sorted_in Tot _). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)