proposition: Lemma sorted_last_key_maxR (s : seq A) leT x y : reflexive leT -> transitive leT -> sorted leT s -> x \in s -> leT x (last y s).
proof: Proof. move=>R T S X; case/orP: (sorted_last_key_max y T S X)=>// /eqP <-. by apply: R. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)