Mv lemma earlier to be able to compile Set_dec earlier.

Lebesgue/Set_theory/Set_def_base.v

@@ -16,6 +16,7 @@ COPYING file for more details.
 
 (** Basic operations on sets (definitions). *)
 
+From Coq Require Import Classical_Pred_Type.
 From Coq Require Import PropExtensionality FunctionalExtensionality.
 
 
@@ -177,6 +178,14 @@ intros HA; induction HA as [x Hx]; exists x; easy.
 intros [x Hx]; eapply ne, Hx.
 Qed.
 
+Lemma nonempty_equiv_alt :
+  forall (A : set U), nonempty A <-> ~ empty A.
+Proof.
+intros A; split; intros HA.
+induction HA as [x Hx]; intros H; apply (H x); easy.
+destruct (not_all_not_ex _ _ HA) as [x Hx]; eapply ne, Hx.
+Qed.
+
 (** Extensionality of sets. *)
 
 Lemma set_ext : forall (A B : set U), same A B -> A = B.