proposition: Lemma sorted_last_key_max (s : seq A) leT x y : transitive leT -> sorted leT s -> x \in s -> (x == last y s) || leT x (last y s).
proof: Proof. move=>T; elim: s x y=>[|z s IH] //= x y H; rewrite inE. case: eqP=>[->|] /= _; first by apply: path_last. by apply: IH (path_sorted H). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)