diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-04 11:07:06 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2013-12-04 11:07:06 +0100 |
| commit | 3339c56fec1b9e9aab6f31c04ddbe3a77b5812ec (patch) | |
| tree | 55a576798fb9f3e162086c0abe2e24d2dc7e411e /theories/Reals | |
| parent | 32f6c4ee62146810c72cb5c86f341c8ca77be909 (diff) | |
Add lemma derivable_pt_lim_atan.
Note: the choice of the derivative comes from derivable_pt_lim_ps_atan
rather than derivable_pt_atan.
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/Ratan.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index b1eb17b21..4bca62706 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -727,6 +727,16 @@ replace (Rsqr x) with (x ^ 2) by (unfold Rsqr; ring). reflexivity. Qed. +Lemma derivable_pt_lim_atan : + forall x, derivable_pt_lim atan x (/(1 + x^2)). +Proof. +intros x. +apply derive_pt_eq_1 with (derivable_pt_atan x). +replace (x ^ 2) with (x * x) by ring. +rewrite <- (Rmult_1_l (Rinv _)). +apply derive_pt_atan. +Qed. + (** * Definition of the arctangent function as the sum of the arctan power series *) (* Proof taken from Guillaume Melquiond's interval package for Coq *) |