proposition: Lemma consec_sort_le leT ks t1 t2 : uniq ks -> {in ks, reflexive leT} -> antisymmetric leT -> transitive leT -> {in ks &, total leT} -> t2 \in ks -> consec (sort leT ks) t1 t2 -> {in ks, forall z, leT z t1 = (z != t2) && leT z t2}.
proof: Proof. set ks' := sort _ _=>U R Asym T Tot T2 C z Z. apply: (@consec_sorted_le leT ks')=>//. - by rewrite sort_uniq. - by move=>x; rewrite mem_sort; apply: R. - by apply: sort_sorted_in Tot _ _. - 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)