proposition: Lemma consec_rconsEP k k1 k2 ks : uniq ks -> k \notin ks -> consec (rcons ks k) k1 k2 <-> if k1 != k then if k2 \notin ks then k2 = k /\ k1 = last k ks else consec ks k1 k2 else k2 \notin rcons ks k.
proof: Proof. move=>U K; rewrite consec_rconsEP' //. case: eqP=>//= /eqP N1; case: ifP=>// N2. split; case=>->; first by case=>ks' ->; rewrite last_rcons. move/esym=>E; split=>//; rewrite -E. have : last k ks != k by rewrite E. move/last_change=>{N1 N2}E. move: ks k U K E; apply: last_ind=>// xs x IH k U K E. by rewrite last_rcons; exists xs. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)