// is now more powerful

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 904a17a9e6bb300eab7b2078f7d970c55caa5e5a..e242cb882d52e527f812d2cbf89457885377c8df 100644 (file)
--- 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.