Reorganization of results.

[helm.git] / matita / library / Z / z.ma

diff --git a/matita/library/Z/z.ma b/matita/library/Z/z.ma
index d8b829ec1da6e60da84bf89fe20c94e80dc72351..64b608cb9524602afa01054b31624d833f9d8d0c 100644 (file)
--- a/matita/library/Z/z.ma
+++ b/matita/library/Z/z.ma
@@ -34,6 +34,11 @@ definition neg_Z_of_nat \def
 [ O \Rightarrow  OZ 
 | (S n)\Rightarrow  neg n].
 
+lemma pos_n_eq_S_n : \forall n : nat.
+  (pos n) = (S n).
+intro.reflexivity. 
+qed.
+
 definition abs \def
 \lambda z.
  match z with