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 : α) : count a [b] = if b = a then 1 else 0

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