fact: Fixpoint nb_occ (z:Z) (l:list Z) {struct l} : nat := match l with | nil => 0%nat | (z' :: l') => match Z.eq_dec z z' with | left _ => S (nb_occ z l') | right _ => nb_occ z l' end end.
imports: List ZArith RelationClasses Morphisms Extraction