proposition: Lemma sort_pairwise_stable T (leT leT' : rel T) : total leT -> forall s : seq T, pairwise leT' s -> sorted [rel x y | leT x y && (leT y x ==> leT' x y)] (sort leT s).
proof: Proof. move=> leT_total s pairwise_s; case Ds: s => // [x s1]. rewrite -{s1}Ds -(mkseq_nth x s) sort_map. apply/homo_sorted_in/sort_iota_stable/(fun _ _ => leT_total _ _)/allss => y z. rewrite !mem_sort !mem_iota !leq0n add0n /= => ys zs /andP [->] /=. by case: (leT _ _); first apply: pairwiseP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)