proposition: Lemma consec_sorted_lt ltT ks t1 t2 : uniq ks -> irreflexive ltT -> antisymmetric ltT -> transitive ltT -> sorted ltT ks -> t2 \in ks -> consec ks t1 t2 -> {in ks, forall z, ltT z t2 = (z == t1) || ltT z t1}.
proof: Proof. move=>U I Asym T S T2 C; move: (consec_mem C)=>T1. have {}Asym : antisymmetric (fun x y => (x == y) || ltT x y). - move=>x y; rewrite (eq_sym y); case: eqP=>//= _. by apply: (Asym x y). have {}T : transitive (fun x y => (x == y) || ltT x y). - move=>x y z; case: eqP=>[->|/eqP _] //=. case: eqP=>[->->|/eqP _ /=]; first by rewrite orbT. by case: eqP=>//= _; apply: T. have {}S : sorted (fun x y => (x == y) || ltT x y) ks. - by apply: sub_sorted S=>x y ->; rewrite orbT. move=>z Z; move/(consec_in U)/(_ z Z): C. rewrite (slt_sorted_leE Asym T S) //. rewrite (sle_sorted_leE Asym T S) //. by rewrite !orbA orbb; case: eqP=>//= ->; rewrite I. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)