proposition: Lemma consecP_inlt (ks : seq A) t1 t2 : uniq ks -> reflect ([/\ t1 \in ks & {in ks, forall z, z <[ks] t2 = z <=[ks] t1}]) (consec ks t1 t2).
proof: Proof. move=>U; apply: (iffP (consecP ks t1 t2)); case=>H1 H2; split. - by apply: slt_memE H1. - by move=>z Z; apply: (hasNL_oo U H1 H2 Z). - by rewrite H2 // sle_refl. by apply: (hasNR_oo U)=>z /H2. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)