New version.

[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 8ab638da8694fe04a6c82d280f12ef7233155e5b..adf85249967c8fe1c402b82dcabbb4839679a44c 100644 (file)
--- 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]).