From 3105f39c45305c860e3d207d9dff915a6ba56be1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 18 Sep 2023 12:39:07 -0700 Subject: [PATCH] Add `iff` versions of two stdlib bool lemmas --- theories/Bool/Bool.v | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 766af385a9e0..dbf49e517aa7 100644 --- 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]