proposition: Lemma none_nb_occ_O : forall (B : Type) (a : A) (l : list (A * B)), find a l = None -> nb_occ a l = 0.
proof: Proof. fix none_nb_occ_O 3. intros B a l; case l; clear l; simpl. intros _; reflexivity. intros p l; case p; clear p; intros a1 b1; simpl. case (eq_bool a a1). intro Abs; discriminate. apply none_nb_occ_O. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)