proposition: Lemma some_nb_occ_Sn : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2}) (a : A) (l : list (A * B)) b, find eqA a l = Some b -> 1 <= nb_occ eqA a l.
proof: Proof. intros A B eqA a l; induction l as [ | [a1 b1] l]. intros; discriminate. intro b; simpl; destruct (eqA a a1) as [_ | _]. auto with arith. intros; apply IHl with b; trivial. Qed.
imports: List Arith