X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpower_derivative.ma;h=dc3f4c828f25c26e716678abdbd13e69c2a132f0;hb=f79585fe2f19c4a545938e189439d87b2611a47a;hp=24656c1d3da9f53f43d170b4837cc765ce1fb138;hpb=45d8e093b732768f58794dc3169e2980257dc7d3;p=helm.git

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index 24656c1d3..dc3f4c828 100644
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -319,8 +319,8 @@ theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n.
    (D[x \sup (2+m)] = (2+m) · x \sup (1+m)).
   conclude
      (D[x \sup (2+m)])
-   = (D[x \sup 1 · x \sup (1+m)]) by _.
-   = (D[x \sup 1] · x \sup (1+m) + x · D[x \sup (1+m)]) by _.
+   = (D[x · x \sup (1+m)]) by _.
+   = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]) by _.
    = (x \sup (1+m) + x · (costante (1+m) · x \sup m)) by _.
 clear H.
    = (x \sup (1+m) + costante (1+m) · x \sup (1+m)) by _.