X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpower_derivative.ma;h=fd58c9564ae12b329e44384d7df14b0b5a07eef0;hb=92ff0c811f55b37004e2ee45dff0859c31857128;hp=e910c8b6a715c4b89beee7fb220659bd0aea9ec5;hpb=5db568e9709437a8ad077130e43ed090970ac1dc;p=helm.git

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index e910c8b6a..fd58c9564 100644
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -277,13 +277,12 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n).
       suppose (0=m) (m_zero). by _ done.
   conclude
      (D[x \sup (1+m)])
-   = (D[x · x \sup m]) by _.
-   = (D[x] · x \sup m + x · D[x \sup m]) by _.
-   = (x \sup m + x · (m · x \sup (pred m))) by _.
-clear H.
-   = (x \sup m + m · (x \sup (1 + pred m))) by _.
-   = (x \sup m + m · x \sup m) by _.
-   = ((1+m) · x \sup m) by _ (timeout=120)
+   = (D[x · x \sup m]).
+   = (D[x] · x \sup m + x · D[x \sup m]).
+   = (x \sup m + x · (m · x \sup (pred m))).
+   = (x \sup m + m · (x \sup (1 + pred m))).
+   = (x \sup m + m · x \sup m).
+   = ((1+m) · x \sup m) by Fmult_one_f Fmult_commutative Fmult_Fplus_distr costante_sum
   done.
 qed.
 
@@ -320,11 +319,11 @@ 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 · 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 _.
-   = (x \sup (1+m) · (costante (2 + m))) by _
+   = (D[x · x \sup (1+m)]).
+   = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]).
+   = (x \sup (1+m) + x · (costante (1+m) · x \sup m)).
+   = (x \sup (1+m) + costante (1+m) · x \sup (1+m)).
+   = ((2+m) · x \sup (1+m)) by Fmult_one_f Fmult_commutative
+     Fmult_Fplus_distr assoc_plus plus_n_SO costante_sum
   done.
-qed.
+qed.
\ No newline at end of file