proposition: Lemma ord_path (s : seq A) leT (x y : A) : transitive leT -> leT x y -> path leT y s -> path leT x s.
proof: Proof. move=>T; elim: s x y=>[|k s IH] x y //= H1 /andP [H2 ->]. by rewrite (T _ _ _ H1 H2). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)