From 2b061073ed17c537a6ea969960e5a3038ed30d05 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 13 Jul 2005 10:20:49 +0000 Subject: [PATCH] use dvariant for associtivity --- helm/matita/library/Z/z.ma | 24 ++++-------------------- 1 file changed, 4 insertions(+), 20 deletions(-) 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. + -- 2.39.2