From 3339c56fec1b9e9aab6f31c04ddbe3a77b5812ec Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 4 Dec 2013 11:07:06 +0100
Subject: Add lemma derivable_pt_lim_atan.

Note: the choice of the derivative comes from derivable_pt_lim_ps_atan
rather than derivable_pt_atan.
---
 theories/Reals/Ratan.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v
index b1eb17b212..4bca627066 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 *)
 
-- 
cgit v1.2.3