X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpower_derivative.ma;fp=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpower_derivative.ma;h=a425dfcc357783ee52a23f8215be3d91265d29b5;hb=765eb07cafb8a06a5027f4569ad06d805aba2488;hp=8e7483e96acf6551e376cc3445736c21cdd97a74;hpb=66ed4f33ff67b9fe0c28ce4a37eee4834e78e115;p=helm.git

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index 8e7483e96..a425dfcc3 100644
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -259,10 +259,13 @@ theorem derivative_power: ∀n:nat. D[X \sup n] = n·X \sup (pred n).
      (D[X \sup (1+m)])
    = (D[X · X \sup m]).
    = (D[X] · X \sup m + X · D[X \sup m]).
-   = (X \sup m + X · (m · X \sup (pred m))) timeout=30.
+   = (X \sup m + X · (m · X \sup (pred m))). 
+   lapply depth=0 Fmult_associative;
+   lapply depth=0 Fmult_commutative;
+   = (X \sup m + m · (X · X \sup (pred m))) by Fmult_associative, Fmult_commutative.
    = (X \sup m + m · (X \sup (1 + pred m))).
    = (X \sup m + m · X \sup m).
-   = ((1+m) · X \sup m) timeout=30 by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
+   = ((1+m) · X \sup m) by Fmult_one_f, Fmult_commutative, Fmult_Fplus_distr, costante_sum
   done.
 qed.