proposition: Lemma consec_next_inj ks t t1 t2 : uniq ks -> t1 \in ks -> consec ks t t1 -> consec ks t t2 -> t1 = t2.
proof: Proof. move=>U T C1 C2; suff N : t != last t1 ks. - by apply: consec_next_inj_nonlast U N C1 C2. by apply: contraL T=>/eqP /(consec_lastE t1 U C1). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)