Merge PR coq#18057: Add iff versions of two stdlib bool lemmas

Reviewed-by: herbelin Co-authored-by: herbelin <[email protected]>
SkySkimmer · Sep 28, 2023 · 41944f5 · 41944f5
2 parents 045c362 + 3105f39
commit 41944f5
Showing 1 changed file with 10 additions and 0 deletions.
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
@@ -739,11 +739,21 @@ Qed.
 
 Notation bool_3 := eq_true_negb_classical (only parsing). (* Compatibility *)
 
+Lemma eq_true_negb_classical_iff : forall b:bool, negb b <> true <-> b = true.
+Proof.
+  destr_bool; intuition.
+Qed.
+
 Lemma eq_true_not_negb : forall b:bool, b <> true -> negb b = true.
 Proof.
   destr_bool; intuition.
 Qed.
 
+Lemma eq_true_not_negb_iff : forall b:bool, b <> true <-> negb b = true.
+Proof.
+  destr_bool; intuition.
+Qed.
+
 Notation bool_6 := eq_true_not_negb (only parsing). (* Compatibility *)
 
 #[global]