update in groud_2 and models

[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 bca5bbf0181a941d650e4bd24190706673f4ac36..a425dfcc357783ee52a23f8215be3d91265d29b5 100644 (file)
--- 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.