proposition: Lemma rcons_lastP x (s : seq A) : reflect (exists s', s = rcons s' (last x s)) (last x s \in s).
proof: Proof. case X : (last x s \in s); constructor; first by apply: rcons_lastX X. case=>s' E; move/negP: X; elim. by rewrite E last_rcons mem_rcons inE eqxx. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)