proposition: Lemma consec_rconsE 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 iffE consec_rconsEP //. case: ifP=>H1 //; case: ifP=>H2 //. by split; [case=>->->; rewrite !eq_refl|case/andP=>/eqP -> /eqP ->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)