proposition: Lemma consec_in (ks : seq A) t1 t2 : uniq ks -> consec ks t1 t2 -> {in ks, forall z, z <[ks] t2 = z <=[ks] t1}.
proof: Proof. by move=>U; case/(consecP_inlt _ _ U). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)