X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpower_derivative.ma;h=a425dfcc357783ee52a23f8215be3d91265d29b5;hb=e880d6eab5e1700f4a625ddcd7d0fa8f0cce2dcc;hp=bca5bbf0181a941d650e4bd24190706673f4ac36;hpb=93cc2a2254a2620000377dfc99a7aaedf2b8ec63;p=helm.git

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index bca5bbf01..a425dfcc3 100644
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -244,6 +244,7 @@ theorem derivative_power: ∀n:nat. D[X \sup n] = n·X \sup (pred n).
    (D[X \sup (1+m)] = (1+m) · X \sup m).
   we need to prove
    (m · (X \sup (1+ pred m)) = m · X \sup m) (Ppred).
+   lapply depth=0 le_n;
    we proved (0 < m ∨ 0=m) (cases).
    we proceed by induction on cases
    to prove (m · (X \sup (1+ pred m)) = m · X \sup m).
@@ -258,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.