A slightly more complicated example.

diff --git a/helm/software/matita/nlibrary/topology/igft3.ma b/helm/software/matita/nlibrary/topology/igft3.ma
index 3abe4af70c4de56aa70c988362f759ba3fd2185d..904a17a9e6bb300eab7b2078f7d970c55caa5e5a 100644 (file)
--- a/helm/software/matita/nlibrary/topology/igft3.ma
+++ b/helm/software/matita/nlibrary/topology/igft3.ma
@@ -194,7 +194,7 @@ nqed.
       | S m ⇒
          match m with
           [ O ⇒ skipfact O
-          | S _ ⇒ S m * skipfact (pred m) * skipfact O ]]
+          | S _ ⇒ S m * skipfact (pred m) * skipfact (pred m) ]]
 **)
 
 ntheorem psym_plus: ∀n,m. n + m = m + n.
@@ -218,7 +218,7 @@ nlemma easy1: ∀n:nat. two * (S n) = two + two * n.
 nqed.
 
 ndefinition skipfact_dom: uuAx.
- @ nat; #n; ncases n [ napply None | #m; ncases m [ napply (Some … O) | #_; napply (Twice … (pred m) O) ]
+ @ nat; #n; ncases n [ napply None | #m; ncases m [ napply (Some … O) | #_; napply (Twice … (pred m) (pred m)) ]
 nqed.
 
 ntheorem skipfact_base_dec:
@@ -237,9 +237,8 @@ ntheorem skipfact_partial:
        | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize; // ]
    ##| #p; #H1; #H2; @2; nnormalize
        [ //
-       | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize
-          [ nrewrite < (plus_n_Sm …); //
-        ##| /2/ ]
+       | #y; *; #a; #E; nrewrite > E; ncases a; nnormalize;
+         nrewrite < (plus_n_Sm …); // ]##]
 nqed.
 
 ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=O) → nat.
@@ -254,6 +253,6 @@ ndefinition skipfact: ∀n:nat. n ◃ mk_powerclass ? (λx: uuax skipfact_dom.x=
          napply (S m * H true * H false) ]
 nqed.
 
-nlemma test: skipfact four ? = eight. ##[##2: napply (skipfact_partial two)]
+nlemma test: skipfact four ? = four * two * two. ##[##2: napply (skipfact_partial two)]
  nnormalize; //.
 nqed.
\ No newline at end of file