proposition: Lemma sorted_ord_index_leq (s : seq A) leT x y : transitive leT -> antisymmetric leT -> sorted leT s -> x \in s -> leT x y -> x != y -> index x s < index y s.
proof: Proof. move=>T As S P H N; elim: s S As P=>[|z s IH] //= P As; rewrite inE !(eq_sym z). case: eqP H P As=>[<-{z} H P As _|Nxz H P As /= X]; first by rewrite eq_sym (negbTE N). case: eqP Nxz P=>[<-{z} Nxy P|Nyz Nxz P]. - by move/Nxy: (path_ord_index_leq T As H P X). by apply: IH X=>//; apply: path_sorted P. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)