proposition: Lemma max_key_last_notin (s : seq A) (leT : rel A) x y : leT y x -> (forall z, z \in s -> leT z x) -> leT (last y s) x.
proof: Proof. elim: s x y=>[|w s IH] //= x y H1 H2; apply: IH. - by apply: (H2 w); rewrite inE eqxx. by move=>z D; apply: H2; rewrite inE D orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)