X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2FZ%2Fplus.ma;h=eeb1bc643fb83fb756978d4de17da9ad813fb761;hb=13ee180b4b982b7a150e8d727ed4b83813ac3fa2;hp=cd565124589d1e20dbac077a384e1aac6fa06125;hpb=f262223fb7b49a191b25d27ecc58818b9d7a357d;p=helm.git

diff --git a/helm/software/matita/library/Z/plus.ma b/helm/software/matita/library/Z/plus.ma
index cd5651245..eeb1bc643 100644
--- a/helm/software/matita/library/Z/plus.ma
+++ b/helm/software/matita/library/Z/plus.ma
@@ -308,7 +308,6 @@ intro.simplify.intros (z y).
 rewrite < Zplus_z_OZ.
 rewrite < (Zplus_z_OZ y).
 rewrite < (Zplus_Zopp x).
-rewrite < (Zplus_Zopp x).
 rewrite < assoc_Zplus.
 rewrite < assoc_Zplus.
 apply eq_f2