proposition: Lemma consec_sorted ks t1 t2 : uniq ks -> sorted ord ks -> t2 \in ks -> consec ks t1 t2 -> {in ks, forall z, ord z t2 = oleq z t1}.
proof: Proof. move=>U S T2 /(consecP_inlt _ _ U) [T1 H] z Z. rewrite -(slt_sortedE S Z T2) -(sle_sortedE S Z T1). by apply: H Z. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)