proposition: Lemma consec_rconsE' y 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 y ks & k1 \in ks] else consec ks k1 k2 else k2 \notin rcons ks k.
proof: Proof. move=>U K; rewrite iffE consec_rconsEP' //. case: ifP=>_ //; case: ifP=>_ //; split. - by case=>X1 /(rcons_lastXP _ y); rewrite X1 eq_refl. case/and3P=>/eqP X1 X2 X3; split=>//. by apply/(rcons_lastXP _ y); rewrite X2 X3. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)