proposition: Lemma rcons_lastX x y (s : seq A) : x \in s -> exists s', s = rcons s' (last y s).
proof: Proof. elim/last_ind: s=>[|ks k IH] //=. by rewrite last_rcons; exists ks. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)