From 11dc90870a5c1afdb1fb3c62a4098db0666dcc93 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Jul 2005 10:15:30 +0000 Subject: [PATCH] removed drop. --- helm/matita/library/Z/z.ma | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma index f59d7b369..aa50a0003 100644 --- 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. -- 2.39.2