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