proposition: Lemma sort_stable T (leT leT' : rel T) : total leT -> transitive leT' -> forall s : seq T, sorted leT' s -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s).
proof: Proof. move=> leT_total leT'_tr s; rewrite sorted_pairwise //. exact: sort_pairwise_stable. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)