proposition: Lemma splitP2r p x y : mem2 p x y -> split2r x y p.
proof: Proof. move=> pxy; have px := mem2l pxy. have:= pxy; rewrite /mem2 (drop_nth x) ?index_mem ?nth_index //. by case/splitP: px => p1 p2; rewrite cat_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)