# Counting in lists #

This file proves basic properties of `List.countP`

and `List.count`

, which count the number of
elements of a list satisfying a predicate and equal to a given element respectively. Their
definitions can be found in `Batteries.Data.List.Basic`

.

### count #

theorem
List.count_singleton'
{α : Type u_1}
[DecidableEq α]
(a : α)
(b : α)
:

List.count a [b] = if b = a then 1 else 0

theorem
List.count_concat
{α : Type u_1}
[DecidableEq α]
(a : α)
(l : List α)
:

List.count a (l.concat a) = (List.count a l).succ