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