X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2Flibrary%2Fnat%2Ftimes.ma;h=953b3a1b630321187f46f9c2199e8b3dde12a928;hb=c87abd26a1fc526042fe177caef69a186aa373be;hp=f9c731bb0e4c85447cffb3d460358ddb9809d2c8;hpb=244d65f63ca6a736b871f9f91328fe8c5524ff05;p=helm.git

diff --git a/helm/matita/library/nat/times.ma b/helm/matita/library/nat/times.ma
index f9c731bb0..953b3a1b6 100644
--- a/helm/matita/library/nat/times.ma
+++ b/helm/matita/library/nat/times.ma
@@ -12,7 +12,7 @@
 (*                                                                        *)
 (**************************************************************************)
 
-set "baseuri" "cic:/matita/nat/times.ma".
+set "baseuri" "cic:/matita/nat/times".
 
 include "logic/equality.ma".
 include "nat/nat.ma".
@@ -34,8 +34,8 @@ theorem times_n_Sm :
 intros.elim n.
 simplify.reflexivity.
 simplify.apply eq_f.rewrite < H.
-transitivity (plus (plus e1 m) (times e1 m)).symmetry.apply assoc_plus.
-transitivity (plus (plus m e1) (times e1 m)).
+transitivity (plus (plus n1 m) (times n1 m)).symmetry.apply assoc_plus.
+transitivity (plus (plus m n1) (times n1 m)).
 apply eq_f2.
 apply sym_plus.
 reflexivity.
@@ -52,11 +52,16 @@ simplify.apply times_n_O.
 simplify.rewrite > H.apply times_n_Sm.
 qed.
 
-theorem times_plus_distr: \forall n,m,p:nat.
-eq nat (times n (plus m p)) (plus (times n m) (times n p)).
-intros.elim n.
+theorem distributive_times_plus : distributive nat times plus.
+simplify.
+intros.elim x.
 simplify.reflexivity.
 simplify.rewrite > H. rewrite > assoc_plus.rewrite > assoc_plus.
-apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? p.
+apply eq_f.rewrite < assoc_plus. rewrite < sym_plus ? z.
 rewrite > assoc_plus.reflexivity.
 qed.
+
+variant times_plus_distr: \forall n,m,p:nat.
+eq nat (times n (plus m p)) (plus (times n m) (times n p))
+\def distributive_times_plus.
+