// is now more powerful

diff --git a/helm/software/matita/nlibrary/topology/igft2.ma b/helm/software/matita/nlibrary/topology/igft2.ma
index 4529b40d540134b02c97ee7afce247cdf9882022..4ca6460d298aa7c25c3aefce96b6a1a86a21dfd4 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft2.ma
+++ b/helm/software/matita/nlibrary/topology/igft2.ma
@@ -135,24 +135,10 @@ nqed.
       | S m ⇒ S 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.
@@ -172,8 +158,8 @@ ntheorem skipfact_partial:
   | #m; #H; @2
      [ nnormalize; @1
      | nnormalize; #y; nchange in ⊢ (% → ?) with (y = pred (pred (two * (natone + m))));
-       nrewrite > (easy1 …); nchange in ⊢ (% → ?) with (y = two * m);
-       #E; nrewrite > E; nassumption ]##]
+       nnormalize; nrewrite < (plus_n_Sm …); nnormalize;
+       #E; nrewrite > E; napply H ]##]
 nqed.
 
 ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.