proposition: Lemma nb_elts_true : forall (P:nat -> Prop)(Pdec : dec P)(n:nat), (forall k, (k < n)%nat -> P k) -> nb_elts Pdec n =n.
proof: Proof. induction n; simpl; intros; auto. case (Pdec n); intros; auto with arith. absurd (P n); auto with arith. Qed.
imports: ALEA(Utheory) ALEA(Sets)