X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fdemo%2Fpower_derivative.ma;h=adf85249967c8fe1c402b82dcabbb4839679a44c;hb=943c8baae10afee070468ab54f4bf86563df2418;hp=8ab638da8694fe04a6c82d280f12ef7233155e5b;hpb=aa5f71baeba0299c0d29be01798f7a1ad13656f9;p=helm.git

diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma
index 8ab638da8..adf852499 100644
--- a/helm/software/matita/library/demo/power_derivative.ma
+++ b/helm/software/matita/library/demo/power_derivative.ma
@@ -264,10 +264,10 @@ theorem derivative_power: ∀n:nat. D[x \sup n] = n·x \sup (pred n).
     case left.
       suppose (0 < m) (m_pos).
       using (S_pred ? m_pos) we proved (m = 1 + pred m) (H1).
-     done.
+     by H1 done.
     case right.
       suppose (0=m) (m_zero). 
-    done.
+    by m_zero, Fmult_zero_f done.
   conclude
      (D[x \sup (1+m)])
    = (D[x · x \sup m]).