X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;fp=helm%2Fmatita%2Flibrary%2FZ%2Ftimes.ma;h=bb5ed67c5bdeb31bc2a98b000e1e92477eba3c9c;hb=3fd6c79ae8d1b2c6e78763c0758a5bb9f95e34b3;hp=6e7a59d16c99d392f81ad7f96c7711d4caecba05;hpb=d35d134356645a09eb72db6e484f3df583123af1;p=helm.git

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.