proposition: Lemma sorted_max_key_last (s : seq A) leT x y : transitive leT -> antisymmetric leT -> sorted leT s -> x \in s -> (forall z, z \in s -> leT z x) -> last y s = x.
proof: Proof. move=>T S; elim: s x y => [|w s IH] //= x y; rewrite inE /=. case: eqP=>[<- /= H1 _ H2 | _ H /= H1 H2]; last first. - apply: IH (path_sorted H) H1 _ => z H3; apply: H2. by rewrite inE /= H3 orbT. case/orP: (path_last T H1)=>[/eqP //|] X. by apply: S; rewrite X H2 ?mem_last. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)