proposition: Lemma sort_sorted T (leT : rel T) : total leT -> forall s, sorted leT (sort leT s).
proof: Proof. move=> leT_total s; apply/sub_sorted/sort_stable => //= [? ? /andP[] //|]. by case: s => // x s; elim: s x => /=. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)