proposition: Lemma rcons_lastXP x y (s : seq A) : reflect (exists s', s = rcons s' x) ((x == last y s) && (x \in s)).
proof: Proof. case: eqP=>[->|N]; first by apply: rcons_lastP. by constructor; case=>s' E; elim: N; rewrite E last_rcons. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)