From 0034d878cbd23062c7312e13d654ac7fd23a01cf Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 6 Dec 2006 15:52:45 +0000 Subject: [PATCH] More simplification using better notation. --- helm/software/matita/library/demo/power_derivative.ma | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/software/matita/library/demo/power_derivative.ma b/helm/software/matita/library/demo/power_derivative.ma index 24656c1d3..dc3f4c828 100644 --- a/helm/software/matita/library/demo/power_derivative.ma +++ b/helm/software/matita/library/demo/power_derivative.ma @@ -319,8 +319,8 @@ theorem derivative_power': ∀n:nat. D[x \sup (1+n)] = (1+n) · x \sup n. (D[x \sup (2+m)] = (2+m) · x \sup (1+m)). conclude (D[x \sup (2+m)]) - = (D[x \sup 1 · x \sup (1+m)]) by _. - = (D[x \sup 1] · x \sup (1+m) + x · D[x \sup (1+m)]) by _. + = (D[x · x \sup (1+m)]) by _. + = (D[x] · x \sup (1+m) + x · D[x \sup (1+m)]) by _. = (x \sup (1+m) + x · (costante (1+m) · x \sup m)) by _. clear H. = (x \sup (1+m) + costante (1+m) · x \sup (1+m)) by _. -- 2.39.2