proposition: Lemma path_ord_index_leq (s : seq A) leT x y : transitive leT -> antisymmetric leT -> leT x y -> path leT y s -> x \in s -> x = y.
proof: Proof. move=>T; elim: s x y=>[|a l IH] //= x y As Lxy. case/andP=>Lya Pal; rewrite inE. case: eqP Lya Pal As=>[<-{a} Lyx _ As _|Nxa Lya Pal /= As' X]. - by apply: As=>//; rewrite Lxy Lyx. by move/Nxa: (IH x a As' (T _ _ _ Lxy Lya) Pal X). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)