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

0 files changed, 0 insertions, 0 deletions