removed dummy rewrite

[helm.git] / helm / software / matita / library / Z / plus.ma

diff --git a/helm/software/matita/library/Z/plus.ma b/helm/software/matita/library/Z/plus.ma
index cd565124589d1e20dbac077a384e1aac6fa06125..eeb1bc643fb83fb756978d4de17da9ad813fb761 100644 (file)
--- 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