proposition: Lemma nth_path_last (s : seq A) leT x0 k i : transitive leT -> i < size s -> path leT k s -> (nth x0 s i == last k s) || leT (nth x0 s i) (last k s).
proof: Proof. move=>T S P. suff : forall z, z \in s -> (z == last k s) || leT z (last k s). - by apply; rewrite mem_nth. move=>z; apply: sorted_last_key_max=>//. by apply: path_sorted P. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)