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

// is now more powerful
---

diff --git a/helm/software/matita/nlibrary/topology/igft2.ma b/helm/software/matita/nlibrary/topology/igft2.ma
index 4529b40d5..4ca6460d2 100644
--- 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.