proposition: Lemma nth_between (s : seq A) ltT x0 k z i : irreflexive ltT -> transitive ltT -> path ltT k s -> ltT (nth x0 (k::s) i) z -> ltT z (nth x0 s i) -> z \notin s.
proof: Proof. move=>I T P H1 H2; apply/negP=>Z; move: H1 H2. case: (leqP i (size s))=>N; last first. - rewrite !nth_default ?(ltnW N) //= => H. by move/(T _ _ _ H); rewrite I. have S : index z s < size s by rewrite index_mem. rewrite -(nth_index x0 Z) !(nth_consS s x0 k). move/(nth_mono_ltn I T N S P)=>K1. move/(nth_mono_ltn I T S (leq_trans K1 S) P); rewrite ltnS. by case: ltngtP K1. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)