proposition: Lemma consec_sorted_le (leT : rel A) ks t1 t2 : uniq ks -> {in ks, reflexive leT} -> antisymmetric leT -> transitive leT -> sorted leT ks -> t2 \in ks -> consec ks t1 t2 -> {in ks, forall z, leT z t1 = (z != t2) && leT z t2}.
proof: Proof. move=>U R Asym T S T2 C; move: (consec_mem C)=>T1. 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 move=>->; case: eqP=>// ->; rewrite R. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)