proposition: Lemma olt_consec_next ks t1 t2 : uniq ks -> t1 <[ks] t2 <-> exists t, consec ks t1 t /\ t <=[ks] t2.
proof: Proof. move=>U; split=>[H|]; last first. - by case=>t [/consecP [X _] /(slt_sle_trans X)]. case/slt_splitL: H U=>ks1 [ks2][-> Nt1t2 N1 N2] /=. rewrite cat_uniq /= negb_or -!andbA. case/and5P=>Uks1 _ /hasPn Nks2 Nt1ks2 Uks2. have H : head t2 ks2 \notin ks1. - move: (mem_head t2 ks2); rewrite inE. by case/orP=>[/eqP ->//|]; apply: Nks2. exists (head t2 ks2); split; last first. - rewrite sle_cat (negbTE H) N2 /= sle_cons (eq_sym t2) Nt1t2 /=. by rewrite sle_head orbT. apply/andP; split. - rewrite slt_cat (negbTE H) (negbTE N1) /= sltL. case: eqP Nt1ks2 (mem_head t2 ks2)=>// -> X. by rewrite inE (negbTE Nt1t2) (negbTE X). rewrite nilp_hasPn; apply: contra H. case/hasP=>x; case/mem_oo. - rewrite cat_uniq /= negb_or Uks1 N1 Nt1ks2 Uks2 /= andbT. by apply/hasPn. move=>_; rewrite !slt_cat /= !slt_cons eqxx /= andbT (negbTE N1) /=. case Xks1 : (x \in ks1)=>/=. - by move/slt_memE=>E; rewrite E in N1. move=>Nxt1; rewrite (negbTE Nxt1) /=; case: ifP=>// _. case/andP=>_ /(sle_slt_trans (@sle_head _ t2 ks2 x))=>+ _. by rewrite slt_irr. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)