X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Fminus.ma;h=10d218d440d7194f2d10e127fddcc3f9eadff05e;hb=6b61a9e6698a7c1936adf217b599e34e65a5e4c9;hp=339e2262c72de402a1d29187e8a41907658038b7;hpb=9edc9828ff3c3d074ccc5547a53eadf092c186d8;p=helm.git

diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma
index 339e2262c..10d218d44 100644
--- a/helm/software/matita/library/nat/minus.ma
+++ b/helm/software/matita/library/nat/minus.ma
@@ -13,8 +13,6 @@
 (**************************************************************************)
 
 
-set "baseuri" "cic:/matita/nat/minus".
-
 include "nat/le_arith.ma".
 include "nat/compare.ma".
 
@@ -78,13 +76,12 @@ qed.
 
 theorem minus_plus_m_m: \forall n,m:nat.n = (n+m)-m.
 intros 2.
-generalize in match n.
-elim m.
+elim m in n ⊢ %.
 rewrite < minus_n_O.apply plus_n_O.
-elim n2.simplify.
+elim n1.simplify.
 apply minus_n_n.
 rewrite < plus_n_Sm.
-change with (S n3 = (S n3 + n1)-n1).
+change with (S n2 = (S n2 + n)-n).
 apply H.
 qed.