diff --git a/Number/Peano/Inf.hs b/Number/Peano/Inf.hs
--- a/Number/Peano/Inf.hs
+++ b/Number/Peano/Inf.hs
@@ -8,9 +8,11 @@
 
 Several lazyness properties:
 
+* @undefined >= 0@,
+
 * @n + undefined >= n@, if @n@ = 0, 1, 2, ...
 
-but @undefined + n >= n@ raises an error.
+but @undefined + n@ raises an error.
 
 * @compare (n + undefined) (n-1) == GT@, if @n@ = 0, 1, 2, ...
 
@@ -45,6 +47,7 @@
     , zeroDiff
     , infDiff
     , (-|)
+    , minimum'
     ) where
 
 import Data.Ratio ((%))
@@ -80,31 +83,35 @@
 {- | 
 Observable infinity value.
 
-The following values are @True@:
+The following values are @True@ for @n@ = 0, 1, 2,... :
 
-* @infinity == infinity@
+* @infinity == infinity@,
 
-* @0 < infinity@, @1 < infinity@, @2 < infinity@, ...
+* @n < infinity@,
 
-* @n + infinity == infinity@,  if @n@ is not the inductive infinity.
+* @n + infinity == infinity@,
 
-* @infinity + n == infinity@
+* @infinity + infinity == infinity@,
 
-* @n * infinity == infinity@,  if @n@ is not the inductive infinity.
+* @infinity + n == infinity@,
 
-* @infinity * n == infinity@
+* @n * infinity == infinity@,
 
-* @n - infinity == 0@,  if @n@ is not the inductive infinity.
+* @infinity * n == infinity@,
 
-* @infinity - n == infinity@,  if @n@ is not the inductive infinity and if @n /= infinity@.
+* @infinity * infinity == infinity@,
 
-The following values rais error messages:
+* @n - infinity == 0@,
 
-* @infinity - infinity@
+* @infinity - n == infinity@.
 
-* @fromEnum infinity@
+The following values raise error messages:
 
-* @toInteger infinity@
+* @infinity - infinity@,
+
+* @fromEnum infinity@,
+
+* @toInteger infinity@.
 -}
 infinity :: Nat
 infinity = Inf
@@ -121,7 +128,7 @@
 
 However, the following values are @True@:
 
-* @0 < inductive_infinity@, @1 < inductive_infinity@, @2 < inductive_infinity@, ...
+* @n < inductive_infinity@, @n@ = 0, 1, 2,...
 
 Note also:
 
@@ -311,7 +318,7 @@
 
             @[inf.. inf] == [inf]@
 
-        Both are reasonable but the second solution would make @enumfrom@ much more eager.
+        Both have sense, but the second solution would make @enumfrom@ more eager.
     -}
     enumFromTo n m = case m `infDiff` n of
 
@@ -385,5 +392,13 @@
 
     minBound = Zero
     maxBound = Inf
+
+{- |
+Minimum of the list elements.
+Works also for empty lists.
+-}
+minimum' :: [Nat] -> Nat
+minimum' = foldr min infinity
+
 
 
diff --git a/peano-inf.cabal b/peano-inf.cabal
--- a/peano-inf.cabal
+++ b/peano-inf.cabal
@@ -1,5 +1,5 @@
 name:           peano-inf
-version:        0.4
+version:        0.5
 synopsis:       Lazy Peano numbers including observable infinity value.
 description:    
     Lazy Peano numbers including observable infinity value.