proposition: Lemma findall_count1 p s : count p s <= 1 -> findall p s = if has p s then [::find p s] else [::].
proof: Proof. rewrite -(findall_size p s); case E: (findall p s)=>[|h t] /=. - by move/nilP: E; rewrite findall_nilp=>/negbTE ->. have ->: has p s by rewrite -(negbK (has p s)) -findall_nilp E. rewrite ltnS leqn0 => /eqP/size0nil Et; move: E; rewrite {t}Et. by rewrite findall_head=>->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq path eqtype choice bigop) pcm(options prelude pred)