Library prosa.util.counting

From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq fintype bigop.

(* Additional lemmas about counting. *)
Section Counting.

  Lemma count_filter_fun :
    ∀ (T: eqType) (l: seq T) P,
      count P l = size (filter P l).

End Counting.