diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 313ca10ebe..30a20f3d12 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -17,6 +17,7 @@
 - in `classical_sets.v`, lemmas `subset_has_lbound`, `subset_has_ubound`
 
 - in `reals.v`, lemmas `sup_setU`, `inf_setU`
+- in `boolp.v`, lemmas `iff_notr`, `iff_not2`
 
 ### Changed
 
diff --git a/theories/boolp.v b/theories/boolp.v
index 2bbde07dac..3c059dc4f2 100644
--- a/theories/boolp.v
+++ b/theories/boolp.v
@@ -366,6 +366,12 @@ Lemma notLR P Q : (P = ~ Q) -> (~ P) = Q. Proof. exact: canLR notK. Qed.
 
 Lemma notRL P Q : (~ P) = Q -> P = ~ Q. Proof. exact: canRL notK. Qed.
 
+Lemma iff_notr (P Q : Prop) : (P <-> ~ Q) <-> (~ P <-> Q).
+Proof. by split=> [/propext ->|/propext <-]; rewrite notK. Qed.
+
+Lemma iff_not2 (P Q : Prop) : (~ P <-> ~ Q) <-> (P <-> Q).
+Proof. by split=> [/iff_notr|PQ]; [|apply/iff_notr]; rewrite notK. Qed.
+
 (* -------------------------------------------------------------------- *)
 (* assia : let's see if we need the simplpred machinery. In any case, we sould
    first try definitions + appropriate Arguments setting to see whether these