Add iff versions of two stdlib bool lemmas

SkySkimmer · Sep 18, 2023 · 3105f39 · 3105f39
1 parent b881f18
commit 3105f39
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]