From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 18 Jan 2010 10:34:24 +0000 (+0000)
Subject: // is now more powerful
X-Git-Tag: make_still_working~3111
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=39b6427bb73ffd7f3149a1efdd73e604f315a058;p=helm.git

// is now more powerful
---

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 904a17a9e..e242cb882 100644
--- a/helm/software/matita/nlibrary/topology/igft3.ma
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -197,24 +197,10 @@ nqed.
           | S _ ⇒ S m * skipfact (pred m) * skipfact (pred m) ]]
 **)
 
-ntheorem psym_plus: ∀n,m. n + m = m + n.
- #n; nelim n
-  [ #m; nelim m; //; #n0; #H;
-    nchange with (natS n0 = natS (n0 + O));
-    nrewrite < H; //
-  | #n0; #H; #m; nchange with (S (n0 + m) = m + S n0);
-    nrewrite > (H …);
-    nelim m; //;
-    #n1; #E; nrewrite > E; //]
+ntheorem psym_plus: ∀n,m. n + m = m + n.//.
 nqed.
 
-nlemma easy1: ∀n:nat. two * (S n) = two + two * n.
- #n; nelim n;//;
- #n0; #H; nnormalize;
- nrewrite > (psym_plus ??);
- nrewrite > H; nnormalize;
- nrewrite > (psym_plus ??);
- //.
+nlemma easy1: ∀n:nat. two * (S n) = two + two * n.//.
 nqed.
 
 ndefinition skipfact_dom: uuAx.