proposition: Lemma max_index_last (s : seq A) (x y : A) : uniq s -> x \in s -> (forall z, z \in s -> index z s <= index x s) -> last y s = x.
proof: Proof. elim: s y=>[|k s IH] y //= /andP [Nk U]; rewrite inE (eq_sym k). case: (x =P k) Nk=>[<-{k} Nk _|_ Nk /= S] /= D; last first. - apply: IH=>// z Z; move: (D z); rewrite inE Z orbT=>/(_ (erefl _)). by case: ifP Z Nk=>// /eqP ->->. suff : nilp s by move/nilP=>->. rewrite /nilp eqn0Ngt -has_predT; apply/hasPn=>z Z. move: (D z); rewrite inE Z orbT=>/(_ (erefl _)). by case: ifP Z Nk=>// /eqP ->->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)