proposition: Lemma sorted_ord_index (s : seq A) ltT x y : irreflexive ltT -> transitive ltT -> sorted ltT s -> x \in s -> ltT x y -> index x s < index y s.
proof: Proof. move=>I T S P H; elim: s S P=>[|z s IH] //= P; rewrite !inE !(eq_sym z). case: eqP H P=>[<-{z} H P _|_ H P /= X]; first by case: eqP H=>[<-|] //; rewrite I. case: eqP H P=>[<-{z} H|_ H]; last first. - by move/path_sorted=>S; rewrite ltnS; apply: IH. by move/(path_mem T)/(_ X)=>/(T _ _ _ H); rewrite I. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)