]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/matita/library/demo/power_derivative.ma
- init_cache_and_tables rewritten using the automation_cache
[helm.git] / helm / software / matita / library / demo / power_derivative.ma
index 8a8fedb68cf65c585d4852710f9df10c52830da9..10cb21835790765e9e7fe64e39bd5b3f862251fb 100644 (file)
@@ -246,7 +246,7 @@ 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).
-     by H1 done.
+      by H1 done.
     case right.
       suppose (0=m) (m_zero). 
     by m_zero, Fmult_zero_f done.