fix PR according to comments

classical_sets.v

@@ -248,24 +248,13 @@ Proof. rewrite propeqE; split => [?|-> //]; exact/eqEsubset. Qed.
 
 Lemma set0P T (X : set T) : (X != set0) <-> (X !=set0).
 Proof.
-split; [move=> X_neq0|by case=> t tX; apply/negP => /eqP X0; rewrite X0 in tX].
-apply/existsp_asboolP; rewrite -(negbK `[exists _, _]); apply/negP.
-rewrite existsbE => /forallp_asboolPn H.
-move/negP : X_neq0; apply; apply/eqP; rewrite funeqE => t; rewrite propeqE.
-move: (H t); by rewrite asboolE.
+split=> [/negP X_neq0|[t tX]]; last by apply/negP => /eqP X0; rewrite X0 in tX.
+by apply: contrapT => /asboolPn/forallp_asboolPn X0; apply/X_neq0/eqP/eqEsubset.
 Qed.
 
 Lemma imageP {A B} (f : A -> B) (X : set A) a : X a -> (f @` X) (f a).
 Proof. by exists a. Qed.
 
-Lemma imsetP T1 T2 (D : set T1) (f : T1 -> T2) b :
-  reflect (exists2 a, a \in D & b = f a) (b \in f @` D).
-Proof.
-apply: (iffP idP) => [|[a aC ->]].
-by rewrite in_setE => -[a Ca <-{b}]; exists a => //; rewrite in_setE.
-by rewrite in_setE; apply/imageP; rewrite -in_setE.
-Qed.
-
 Lemma sub_image_setI {A B} (f : A -> B) (X Y : set A) :
   f @` (X `&` Y) `<=` f @` X `&` f @` Y.
 Proof. by move=> b [x [Xa Ya <-]]; split; apply: imageP. Qed.
@@ -312,8 +301,8 @@ Proof. by move=> sXZ sYZ a; apply: or_ind; [apply: sXZ|apply: sYZ]. Qed.
 
 Lemma subUset T (X Y Z : set T) : (Y `|` Z `<=` X) = ((Y `<=` X) /\ (Z `<=` X)).
 Proof.
-rewrite propeqE; split => [H|H]; first by split => x Hx; apply H; [left|right].
-move=> x [] Hx; [exact: (proj1 H)|exact: (proj2 H)].
+rewrite propeqE; split => [|[YX ZX] x]; last by case; [exact: YX | exact: ZX].
+by move=> sYZ_X; split=> x ?; apply sYZ_X; [left | right].
 Qed.
 
 Lemma subsetI A (X Y Z : set A) : (X `<=` Y `&` Z) = ((X `<=` Y) /\ (X `<=` Z)).
@@ -371,18 +360,11 @@ Proof. move=> p; rewrite /setU predeqE => a; tauto. Qed.
 Lemma setUC A : commutative (@setU A).
 Proof. move=> p q; rewrite /setU predeqE => a; tauto. Qed.
 
-Lemma in_setU T (X Y : set T) x : (x \in X `|` Y) = (x \in X) || (x \in Y) :> Prop.
-Proof.
-rewrite propeqE; split => [ | ]; last first.
-  move/orP => -[]; rewrite 2!in_setE => ?; by [left|right].
-rewrite in_setE => -[?|?]; apply/orP; rewrite 2!in_setE; tauto.
-Qed.
-
 Lemma set0U T (X : set T) : set0 `|` X = X.
-Proof. rewrite funeqE => t; rewrite propeqE; split; by [case|right]. Qed.
+Proof. by rewrite funeqE => t; rewrite propeqE; split; [case|right]. Qed.
 
 Lemma setU0 T (X : set T) : X `|` set0 = X.
-Proof. rewrite funeqE => t; rewrite propeqE; split; by [case|left]. Qed.
+Proof. by rewrite funeqE => t; rewrite propeqE; split; [case|left]. Qed.
 
 Lemma setU_eq0 T (X Y : set T) : (X `|` Y = set0) = ((X = set0) /\ (Y = set0)).
 Proof. by rewrite -!subset0 subUset. Qed.