proposition: Lemma seq_last_in (s : seq A) x : last x s \notin s -> s = [::].
proof: Proof. case: (lastP s)=>{s} // s y; case: negP=>//; elim; rewrite last_rcons. by elim: s=>[|y' s IH]; rewrite /= inE // IH orbT. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)