proposition: Lemma has_nilP xs : reflect (has predT xs) (xs != [::]).
proof: Proof. by case: xs=>[|x xs]; constructor. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)