proposition: Lemma path_lastR (s : seq A) leT x : reflexive leT -> transitive leT -> path leT x s -> leT x (last x s).
proof: Proof. by move=>R T P; case: eqP (path_last T P)=>// <- _; apply: R. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)