diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index f908a9cfe0..cae19b75e0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -4,8 +4,8 @@
 
 ### Added
 
-- in `boolp.v`, lemmas for classical reasoning `existsNP`, `existsP`,
-  `forallNP`, `forallP`, `imply_classic`, `orC`.
+- in `boolp.v`, lemmas for classical reasoning `existsNP`, `existsPN`,
+  `forallNP`, `forallPN`, `Nimply`, `orC`.
 - in `classical_sets.v`, definitions for supremums: `ul`, `lb`,
   `supremum`
 - in `ereal.v`:
diff --git a/theories/boolp.v b/theories/boolp.v
index e7ae124990..7ba49311ae 100644
--- a/theories/boolp.v
+++ b/theories/boolp.v
@@ -140,7 +140,6 @@ Qed.
 Lemma gen_choiceMixin {T : Type} : Choice.mixin_of T.
 Proof. by case: classic. Qed.
 
-
 Lemma pdegen (P : Prop): P = True \/ P = False.
 Proof. by have [p|Np] := pselect P; [left|right]; rewrite propeqE. Qed.
 
@@ -561,7 +560,7 @@ split => [[x Px h]|/asboolP]; [exact: Px|].
 by rewrite asbool_neg => /existsp_asboolPn.
 Qed.
 
-Lemma existsP (T : Type) (P : T -> Prop) :
+Lemma existsPN (T : Type) (P : T -> Prop) :
   (exists x : T, P x) <-> (~ forall x : T, ~ P x).
 Proof.
 split => [[x Px h]|/asboolP]; [exact: (h x)|].
@@ -575,16 +574,16 @@ split => [h [x Px]|/asboolP]; [exact: (h x)|].
 by rewrite asbool_neg => /forallp_asboolPn.
 Qed.
 
-Lemma forallP (T : Type) (P : T -> Prop) :
+Lemma forallPN (T : Type) (P : T -> Prop) :
   (forall x : T, P x) <-> (~ exists x : T, ~ P x).
 Proof.
 split => [h [x px]|]; [exact/px/h|move=> /forallNP h x].
 by move/contrapT : (h x).
 Qed.
 
-Lemma imply_classic (P Q : Prop) : (P /\ ~ Q) <-> ~ (P -> Q).
+Lemma Nimply (P Q : Prop) : ~ (P -> Q) <-> (P /\ ~ Q).
 Proof.
-split => [[p nq pq]|/asboolP]; [exact/nq/pq|].
+split=> [/asboolP|[p nq pq]]; [|exact/nq/pq].
 by rewrite asbool_neg => /imply_asboolPn.
 Qed.
 
diff --git a/theories/ereal.v b/theories/ereal.v
index 99a59013f2..f947860ec1 100644
--- a/theories/ereal.v
+++ b/theories/ereal.v
@@ -476,7 +476,7 @@ have [Spoo|Spoo] := pselect (S +oo).
   by exists +oo; split; [apply/ereal_ub_pinfty | apply/lbP => /= y /ubP; apply].
 have [r Sr] : exists r, S r%:E.
   move: S0 Snoo Spoo => [[r Sr _ _|//|Snoo Snoo1 Spoo]]; first by exists r.
-  apply/existsP => nS; move: Snoo1; apply; apply/eqP; rewrite predeqE.
+  apply/existsPN => nS; move: Snoo1; apply; apply/eqP; rewrite predeqE.
   by case=> // r; split => // /nS.
 set U := [set x | (real_of_er_def r @` S) x ].
 have [ubU|/set0P/negP] := pselect (ub U !=set0); last first.
@@ -545,7 +545,7 @@ have : ~ ub S (ereal_sup S - e%:num%:E)%E.
   move/ub_ereal_sup; apply/negP.
   by rewrite -ltNge Sr lte_subl_addr lte_fin ltr_addl.
 move/asboolP; rewrite asbool_neg; case/existsp_asboolPn => /= x.
-case/imply_classic => ? ?; exists x; split => //.
+case/Nimply => ? ?; exists x; split => //.
 by rewrite ltNge; apply/negP.
 Qed.
 
diff --git a/theories/reals.v b/theories/reals.v
index e38a56e787..e503d8424e 100644
--- a/theories/reals.v
+++ b/theories/reals.v
@@ -327,7 +327,7 @@ split; last first.
   move=> h [x] /ubP hle; case/(_ x): h => y /hle.
   by rewrite leNgt => /negbTE ->.
 move/forallNP => h x; have {h} := h x.
-move=> /ubP /existsNP => -[y /imply_classic[Ey /negP]].
+move=> /ubP /existsNP => -[y /Nimply[Ey /negP]].
 by rewrite -ltNge => ltx; exists y.
 Qed.