proposition: Lemma index_rcons a x xs : index a (rcons xs x) = if a \in xs then index a xs else if a == x then size xs else (size xs).+1.
proof: Proof. rewrite eq_sym; elim: xs=>[|y xs IH] //=. rewrite inE eq_sym; case: eqP=>//= _. by rewrite IH; case: ifP=>// _; case: eqP. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)