From d619e901add481f1660d098e86bd3dcf02fc82e2 Mon Sep 17 00:00:00 2001
From: courant
Date: Thu, 14 Nov 2002 13:43:33 +0000
Subject: nettoyage preuve limit_comp

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3231 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Reals/Rlimit.v | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v
index 25b4ea7a69..dc849132f1 100644
--- a/theories/Reals/Rlimit.v
+++ b/theories/Reals/Rlimit.v
@@ -501,14 +501,15 @@ Qed.
 Lemma limit_comp:(f,g:R->R)(Df,Dg:R->Prop)(l,l':R)(x0:R)
    (limit1_in f Df l x0)->(limit1_in g Dg l' l)->
    (limit1_in [x:R](g (f x)) (Dgf Df Dg f) l' x0).
-Unfold limit1_in;Unfold limit_in;Simpl;Intros;
- Elim (H0 eps H1);Clear H0;Intros;Elim H0;Clear H0;Intros;
- Elim (H x H0);Clear H;Intros;Elim H;Clear H;Intros;
- Split with x1;Split;Auto;Intros;
- Elim H4;Clear H4;Intros;Unfold Dgf in H4;Elim H4;Clear H4;Intros;
- Generalize (H3 x2 (conj (Df x2) (Rlt (R_dist x2 x0) x1) H4 H5));
- Intro;Exact (H2 (f x2) (conj (Dg (f x2)) (Rlt (R_dist (f x2) l) x)
-            H6 H7)).
+Unfold limit1_in limit_in Dgf;Simpl.
+Intros f g Df Dg l l' x0 Hf Hg eps eps_pos.
+Elim (Hg eps eps_pos).
+Intros alpg lg.
+Elim (Hf alpg).
+2: Tauto.
+Intros alpf lf.
+Exists alpf.
+Intuition.
 Qed.
 
 (*********)
-- 
cgit v1.2.3