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 k2 = head k ks else k2 != k /\ ks = [::] else k2 != k /\ consec ks k1 k2.
proof: Proof. move=>U /(consec_consEP' _ _ U)=>->. case: ifP=>// E1; case: ifP=>//. by case: {U}ks=>//= x ks E2; split=>[[]|->]. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)