diff options
| author |  mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-07-03 18:27:15 +0000 |
|---|---|---|
| committer | mayero <mayero@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-07-03 18:27:15 +0000 |
| commit | 533d30df924cbdd9e0ef01e4d9fb8a48e201e6e8 (patch) | |
| tree | feeabb1b13161c34a88b41a6a4f59a62f9961f8b /theories/Reals/Rderiv.v | |
| parent | 9013e6d80b26b177fbcd10a706f271ca4b576585 (diff) | |
ajouts
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@553 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rderiv.v')
| -rw-r--r-- | theories/Reals/Rderiv.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index d36ca5897..680a18ab9 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -399,6 +399,14 @@ Intros;Generalize (H2 x1 H3);Clear H2;Intro;Rewrite Ropp_mul1 in H2; Save. (*********) +Lemma Dminus:(D:R->Prop)(df,dg:R->R)(f,g:R->R)(x0:R) + (D_in f df D x0)->(D_in g dg D x0)-> + (D_in [x:R](Rminus (f x) (g x)) [x:R](Rminus (df x) (dg x)) D x0). +Unfold Rminus;Intros;Generalize (Dopp D g dg x0 H0);Intro; + Apply (Dadd D df [x:R](Ropp (dg x)) f [x:R](Ropp (g x)) x0);Assumption. +Save. + +(*********) Lemma Dx_pow_n:(n:nat)(D:R->Prop)(x0:R) (D_in [x:R](pow x n) [x:R](Rmult (INR n) (pow x (minus n (1)))) D x0). |