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