Numbers: finish files NStrongRec and NDefOps

 - NStrongRec provides a "strong" recursor based on the usual one:
   recursive calls can be done here on any lower value.
   See binary log in NDefOps for an example of use.

 - NDefOps contains alternative definitions of usual operators
   (add, mul, ltb, pow, even, half, log)
   via usual or strong recursor, and proofs of correctness and/or
   of equivalence with axiomatized operators.

 These files were in the archive but not being compiled,
 some proofs of correction for functions defined there were missing.

 By the way, some more iff-style lemmas in Bool.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12476 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 19 insertions, 11 deletions

diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index bc42c6564..66ab6f1c8 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -54,21 +54,22 @@ Qed.
 
 Lemma not_true_is_false : forall b:bool, b <> true -> b = false.
 Proof.
-  destruct b.
-  intros.
-  red in H; elim H.
-  reflexivity.
-  intros abs.
-  reflexivity.
+  destruct b; intuition.
 Qed.
 
 Lemma not_false_is_true : forall b:bool, b <> false -> b = true.
 Proof.
-  destruct b.
-  intros.
-  reflexivity.
-  intro H; red in H; elim H.
-  reflexivity.
+  destruct b; intuition.
+Qed.
+
+Lemma not_true_iff_false : forall b, b <> true <-> b = false.
+Proof.
+  destruct b; intuition.
+Qed.
+
+Lemma not_false_iff_true : forall b, b <> false <-> b = true.
+Proof.
+  destruct b; intuition.
 Qed.
 
 (**********************)
@@ -547,6 +548,13 @@ Proof.
   intros b1 b2; case b1; case b2; intuition.
 Qed.
 
+Lemma eq_iff_eq_true : forall b1 b2, b1 = b2 <-> (b1 = true <-> b2 = true).
+Proof.
+  split.
+  intros; subst; intuition.
+  apply eq_true_iff_eq.
+Qed.
+
 Notation bool_1 := eq_true_iff_eq (only parsing). (* Compatibility *)
 
 Lemma eq_true_negb_classical : forall b:bool, negb b <> true -> b = true.