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