From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 13 Jul 2005 10:20:49 +0000 (+0000)
Subject: use dvariant for associtivity
X-Git-Tag: pre_notation~20
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2b061073ed17c537a6ea969960e5a3038ed30d05;p=helm.git

use dvariant for associtivity
---

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index aa50a0003..11dd836f6 100644
--- a/helm/matita/library/Z/z.ma
+++ b/helm/matita/library/Z/z.ma
@@ -331,23 +331,7 @@ rewrite > Zplus_Zsucc (Zplus (pos e1) y).
 apply eq_f.assumption.
 qed.
 
-theorem assoc_Zplus : 
-\forall x,y,z:Z. eq Z (Zplus x (Zplus y z)) (Zplus (Zplus x y) z).
-intros.elim x.simplify.reflexivity.
-elim e1.rewrite < (Zpred_Zplus_neg_O (Zplus y z)).
-rewrite < (Zpred_Zplus_neg_O y).
-rewrite < Zplus_Zpred.
-reflexivity.
-rewrite > Zplus_Zpred (neg e).
-rewrite > Zplus_Zpred (neg e).
-rewrite > Zplus_Zpred (Zplus (neg e) y).
-apply eq_f.assumption.
-elim e2.rewrite < Zsucc_Zplus_pos_O.
-rewrite < Zsucc_Zplus_pos_O.
-rewrite > Zplus_Zsucc.
-reflexivity.
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (pos e1).
-rewrite > Zplus_Zsucc (Zplus (pos e1) y).
-apply eq_f.assumption.
-qed.
+variant assoc_Zplus : 
+\forall x,y,z:Z. eq Z (Zplus (Zplus x y) z) (Zplus x (Zplus y z))
+\def associative_Zplus.
+