proposition: Lemma mem2_last y0 p x : mem2 p x (last y0 p) = (x \in p).
proof: Proof. apply/idP/idP; first exact: mem2l; rewrite -index_mem /mem2 => p_x. by rewrite -nth_last -(subnKC p_x) -nth_drop mem_nth // size_drop subnSK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)