proposition: Lemma consec_sort_lt ltT ks t1 t2 : irreflexive ltT -> antisymmetric ltT -> transitive ltT -> {in ks &, total (fun x y => (x == y) || ltT x y)} -> uniq ks -> t2 \in ks -> consec (sort (fun x y => (x == y) || ltT x y) ks) t1 t2 -> {in ks, forall z, ltT z t2 = (z == t1) || ltT z t1}.
proof: Proof. set ks' := sort _ _=>I asym T Tot U T2 C z Z. apply: (@consec_sorted_lt ltT ks')=>//. - by rewrite sort_uniq. - by apply: sort_sorted_in_lt. - by rewrite mem_sort. by rewrite mem_sort. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)