proposition: Lemma consec_next_inj_nonlast ks t t1 t2 t3 : uniq ks -> t != last t3 ks -> consec ks t t1 -> consec ks t t2 -> t1 = t2.
proof: Proof. move=>U N C1 C2. have K1 : t1 \in ks by apply: contraR N=>/(consec_lastE t3 U C1) ->. have K2 : t2 \in ks by apply: contraR N=>/(consec_lastE t3 U C2) ->. case/andP: C1 C2=>T1 + /andP [T2]. rewrite !nilp_hasPn => /hasPn H1 /hasPn H2. move: (@slt_total _ ks t1 t2 K1); case/or3P=>[/eqP->|L1|L2] //. - move: (H2 t1)=>/contraL/(_ erefl); apply: contraNeq=>_. by apply/mem_oo. move: (H1 t2)=>/contraL/(_ erefl); apply: contraNeq=>_. by apply/mem_oo. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq path interval order) pcm(options prelude ordtype seqext slice useqord uslice)