proposition: Lemma none_nb_occ_O : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) (a : A) (l : list (A * B)), find eqA a l = None -> nb_occ eqA a l = 0.
proof: Proof. intros A B eqA a l; induction l as [ | [a1 b1] l]; trivial; simpl. destruct (eqA a a1) as [a_eq_a1 | a_diff_a1]; intros. discriminate. apply IHl; trivial. Qed.
imports: List Arith