proposition: Lemma some_nb_occ_Sn : forall (B : Type) (a : A) (l : list (A * B)) b, find a l = Some b -> 1 <= nb_occ a l.
proof: Proof. fix some_nb_occ_Sn 3. intros B a l; case l; clear l; simpl. intros b Abs; discriminate. intros p l b; case p; clear p; simpl. intros a1 b1; case (eq_bool a a1). intros _; apply le_n_S; apply Nat.le_0_l. apply some_nb_occ_Sn. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)