use dvariant for associtivity

diff --git a/helm/matita/library/Z/z.ma b/helm/matita/library/Z/z.ma
index aa50a000325a9ce7e98acce9f6758e4ae0f588fb..11dd836f667b6ed884753f80ec88ac86e731e8d7 100644 (file)
--- 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.
+