Script fixed (it did not compile due to a mistake before committing).

[helm.git] / helm / software / matita / library / demo / power_derivative.ma

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index 9e59079bd8daf9489fc66a5d1fb1befc3a352ad5..fd58c9564ae12b329e44384d7df14b0b5a07eef0 100644 (file)
--- 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=30)
+   = (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.
\ No newline at end of file