removed drop.

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

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index f59d7b369f8607454b24ebc4c3f74c617f2e65ed..aa50a000325a9ce7e98acce9f6758e4ae0f588fb 100644 (file)
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -310,11 +310,10 @@ qed.
 
 
 theorem associative_Zplus: associative Z Zplus.
-(* change with (\forall x,y,z. eq ?(Zplus (Zplus x y) z) (Zplus x (Zplus y z))).*)
-simplify.
+change with (\forall x,y,z. eq ?(Zplus (Zplus x y) z) (Zplus x (Zplus y z))).
+(* simplify. *) 
 intros.elim x.simplify.reflexivity.
 elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
-drop.
 rewrite < (Zpred_Zplus_neg_O y).
 rewrite < Zplus_Zpred.
 reflexivity.