run check_if_goal_is_solved on all goals (active+passive)

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