proposition: Lemma consec_consEP' k k1 k2 ks : uniq ks -> k \notin ks -> consec (k::ks) k1 k2 <-> if k1 == k then if k2 \in ks then ks = k2 :: behead ks else k2 != k /\ ks = [::] else k2 != k /\ consec ks k1 k2.
proof: Proof. move=>U N; split; last first. - case: (k1 =P k)=>[->{k1}|/eqP Nk1k [Nk2]]; last first. - case/consecP=>H1; move=> H2; apply/consecP. rewrite slt_cons (negbTE Nk1k) /= H1 andbT; split=>//. apply: contra H2=>/hasP [x H2 _]; apply/hasP; exists x=>//. move: H2; case/mem_oo; first by rewrite /= N. rewrite !slt_cons inE (negbTE Nk1k) Nk2 /=; case: eqVneq=>//= _ Hx Hx1 Hx2. by apply/mem_oo. case K2 : (k2 \in ks). - move=>E; rewrite {K2}E /= in N U *. rewrite inE negb_or in N. case/andP: U=>U1 U2; case/andP: N=>N1 N2. by apply: consec_hd2. case=>Nk2k E; rewrite {ks N U K2}E. apply/consecP; rewrite sltL; split=>//. apply/hasPn=>x; apply: contraL=>_; apply: contra Nk2k. by case/mem_oo=>//; rewrite inE sltL => /eqP->; rewrite eqxx. case: (k1 =P k)=>[->|/eqP Nk1k]; last first. - move/consecP; rewrite slt_cons (negbTE Nk1k) /=. case=>/andP [Nk2k H1 H2]; split=>//; apply/consecP; split=>//. apply: contra H2=>/hasP [x] H _. apply/hasP; exists x=>//. case/mem_oo: H=>// Hx Hx1 Hx2. apply/mem_oo=>/=; first by rewrite N. rewrite inE !slt_cons (negbTE Nk1k) (negbTE Nk2k) /=. by case: eqVneq=>[E|_] //=; rewrite -E Hx in N. case K2: (k2 \in ks)=>/consecP []; rewrite sltL => Nk2k; last first. - move=>H; split=>//; apply/nilP; rewrite nilp_hasPn. apply: contra H=>/hasP [x X _]; apply/hasP; exists x=>//. apply/mem_oo; first by rewrite /= N. rewrite inE sltL slt_cons X Nk2k /= orbT. case: (x =P k)=>//= [E|_]; first by rewrite -E X in N. by split=>//; apply: slt_memI=>//; rewrite K2. case: ks U N K2=>//= x ks; rewrite !inE negb_or. case/andP=>Nkxs U /andP [Nkx Nks] K2 H; congr (_ :: _). case/orP: K2=>[/eqP->|K2] //. apply: contraNeq H=>?; apply/hasP; exists x=>//. apply/mem_oo; first by rewrite /= inE negb_or Nkx Nks Nkxs. rewrite sltL slt_cons sltL !inE eqxx /= orbT Nk2k /= (eq_sym x) (negbTE Nkx) /=. by split=>//; rewrite eq_sym. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)