From 8907c227f5c456f14617890946aa808ef522d7da Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 9 Sep 2009 16:10:59 +0000
Subject: Znumtheory + Zdiv enriched with stuff from ZMicromega, misc
 improvements

 Mostly results about Zgcd (commutativity, associativity, ...).
 Slight improvement of ZMicromega.

 Beware: some lemmas of Zdiv/ Znumtheory were asking for
 too strict or useless hypothesis. Some minor glitches may occur.

 By the way, some iff lemmas about negb in Bool.v

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12313 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Bool/Bool.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'theories/Bool')

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 2995f0515..dcb10f3cf 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -202,6 +202,16 @@ Proof.
   destruct b; trivial.
 Qed.
 
+Lemma negb_true_iff : forall b, negb b = true <-> b = false.
+Proof.
+ destruct b; intuition.
+Qed.
+
+Lemma negb_false_iff : forall b, negb b = false <-> b = true.
+Proof.
+ destruct b; intuition.
+Qed.
+
 
 (********************************)
 (** * Properties of [orb]     *)
-- 
cgit v1.2.3