proposition: Lemma mem2_index (T : eqType) (x y : T) (s : seq T) : uniq s -> y \in s -> mem2 s x y = (index x s <= index y s).
proof: Proof. have [|xNs _ y_s] := boolP (x \in s); last first. by rewrite mem2lf // (memNindex xNs) leqNgt index_mem y_s. elim: s => //= z s IHs x_s /andP[zNs uniq_s] y_s; rewrite mem2_cons. rewrite y_s; have [-> //|zDx] := eqVneq z x. have [<-|zDy] := eqVneq z y;first by rewrite mem2rf. rewrite !inE ?[_ == z]eq_sym ?(negbTE zDy) ?(negbTE zDx) /= in x_s y_s. exact: IHs. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)