proposition: Lemma path_mem (s : seq A) leT x y : transitive leT -> path leT x s -> y \in s -> leT x y.
proof: Proof. move=>T; elim: s x=>[|z s IH] x //= /andP [O P]. rewrite inE; case/orP=>[/eqP -> //|]. by apply: IH; apply: ord_path O P. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)