proposition: Lemma path_last (s : seq A) leT x : ssrbool.transitive leT -> path leT x s -> (x == last x s) || leT x (last x s).
proof: Proof. move=>T /(order_path_min T) /allP; case: s=>[|a s] H /=. - by rewrite eqxx. by rewrite (H (last a s)) ?orbT // mem_last. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)