proposition: Lemma olt_consec_prev ks t1 t2 : uniq ks -> t1 <[ks] t2 <-> exists t, t1 <=[ks] t /\ consec ks t t2.
proof: Proof. move=>U; split=>[H|]; last first. - by case=>t [H1] /consecP [H2 _]; apply: (sle_slt_trans H1 H2). case/slt_splitL: H U=>ks1 [ks2][-> Nt1t2 N1 N2] /=. rewrite cat_uniq /= negb_or /= -!andbA. case/and5P=>Uks1 Nt1ks1 /hasPn Hks2 Nt1ks2 Uks2. case X : (t2 \in ks2); last first. - have L : last t1 ks2 \notin ks1. - move: (mem_last t1 ks2); rewrite inE. by case/orP=>[/eqP ->//|H]; apply: Hks2. exists (last t1 ks2); split. - by rewrite sle_cat (negbTE N1) sleL andbT. apply/andP; split. - rewrite slt_cat (negbTE N2) (negbTE L) /= slt_cons (eq_sym t2) Nt1t2 /=. move: (mem_last t1 ks2); rewrite inE=>/orP [->//|H]. by rewrite slt_memI ?X ?orbT. rewrite nilp_hasPn; apply: contra L; case/hasP=>x + _; case/mem_oo. - rewrite cat_uniq /= negb_or Uks1 Uks2 Nt1ks1 Nt1ks2 /= andbT. by apply/hasPn. move=>_; rewrite !slt_cat (negbTE N2) !slt_cons (eq_sym t2) Nt1t2 /=. case Xks1 : (x \in ks1)=>/=; first by move/slt_memE. case/orP=>// /andP [Nxt1]; rewrite (negbTE Nxt1) /=. case/orP=>[/eqP/last_nochange|/[swap] Xp1]. - by rewrite (negbTE Nt1ks2)=>/eqP ->. move: (@sle_last _ x t1 ks2)=>/(_ Uks2 (slt_memE Xp1)) Z. by move/(sle_slt_trans Z); rewrite slt_irr. case/splitP: {ks2} X Hks2 Nt1ks2 Uks2=>p1 p2 H2. rewrite mem_cat cat_uniq /= negb_or rcons_uniq mem_rcons inE. rewrite (negbTE Nt1t2) /= -!andbA. case/andP=>Nt1p1 Nt1p2 /and4P [Nt2p1 Up1 /hasPn Hp2 Up2]. have L : last t1 p1 \notin ks1. - move: (mem_last t1 p1); rewrite inE. case/orP=>[/eqP ->//|H]; apply: H2. by rewrite mem_cat mem_rcons inE H orbT. exists (last t1 p1); split. - by rewrite sle_cat (negbTE Nt1ks1) sleL andbT. apply/andP; split. - rewrite slt_cat (negbTE N2) (negbTE L) /= slt_cons (eq_sym t2) Nt1t2 /=. rewrite slt_cat mem_rcons inE eq_refl /= slt_rcons (negbTE Nt2p1) eq_refl /=. by move: (mem_last t1 p1); rewrite inE=>/orP [->|->] //=; rewrite orbT. rewrite nilp_hasPn; apply: contra L; case/hasP=>x. case/mem_oo. - rewrite cat_uniq /= cat_uniq mem_cat !negb_or mem_rcons rcons_uniq negb_or Uks1 N1 Nt1t2 Nt1p1 Nt1p2 Nt2p1 Up1 Up2 /= andbT. by apply/andP; split; apply/hasPn. move=>_; rewrite !slt_cat !slt_cons !slt_cat !mem_rcons !inE (negbTE N2) (eq_sym t2) Nt1t2 /= eqxx /=. case Xks1 : (x \in ks1)=>/=; first by move/slt_memE. case/orP=>// /andP [Nxt1]; rewrite (negbTE Nxt1) /=. case/orP=>[/eqP/last_nochange|/[swap]]. - rewrite (negbTE Nt1p1)=>/eqP ->/=. by rewrite slt_cons eqxx. rewrite slt_rcons (negbTE Nt2p1) eqxx /= orbF => Xp1. rewrite Xp1 orbT slt_rcons Xp1 sltNge. by move: (@sle_last _ x t1 p1)=>/(_ Up1 Xp1) ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)