From 3fd6c79ae8d1b2c6e78763c0758a5bb9f95e34b3 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 21 Jul 2005 14:34:17 +0000
Subject: [PATCH] S_pred moved from Z/times.ma to nat/orders.ma

---
 helm/matita/library/Z/times.ma    |  5 -----
 helm/matita/library/nat/orders.ma | 10 +++++++---
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/helm/matita/library/Z/times.ma b/helm/matita/library/Z/times.ma
index 6e7a59d16..bb5ed67c5 100644
--- a/helm/matita/library/Z/times.ma
+++ b/helm/matita/library/Z/times.ma
@@ -38,11 +38,6 @@ simplify.reflexivity.
 simplify.reflexivity.
 qed.
 
-(* da spostare in nat/order *)
-theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
-intro.elim n.apply False_ind.exact not_le_Sn_O O H.
-apply eq_f.apply pred_Sn.
-qed.
 
 (*
 theorem symmetric_Ztimes : symmetric Z Ztimes.
diff --git a/helm/matita/library/nat/orders.ma b/helm/matita/library/nat/orders.ma
index d4979231d..34cd6f6a3 100644
--- a/helm/matita/library/nat/orders.ma
+++ b/helm/matita/library/nat/orders.ma
@@ -83,6 +83,12 @@ apply H.assumption.
 apply le_S_S_to_le.assumption.
 qed.
 
+(* ??? this needs not le *)
+theorem S_pred: \forall n:nat.lt O n \to eq nat n (S (pred n)).
+intro.elim n.apply False_ind.exact not_le_Sn_O O H.
+apply eq_f.apply pred_Sn.
+qed.
+
 (* le vs. lt *)
 theorem lt_to_le : \forall n,m:nat. lt n m \to le n m.
 simplify.intros.elim H.
@@ -150,6 +156,4 @@ intros.simplify.right.exact not_le_Sn_O n1.
 intros 2.simplify.intro.elim H.
 left.apply le_S_S.assumption.
 right.intro.apply H1.apply le_S_S_to_le.assumption.
-qed.
-
-
+qed.
\ No newline at end of file
-- 
2.39.2