diff options
author | courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 13:43:33 +0000 |
---|---|---|
committer | courant <courant@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-14 13:43:33 +0000 |
commit | d619e901add481f1660d098e86bd3dcf02fc82e2 (patch) | |
tree | b6929063e57cee51f9594734fce0103e4cc0ed40 /theories/Reals/Rlimit.v | |
parent | e278df43db70bbda7d9f4b95d5662a14919d64c1 (diff) |
nettoyage preuve limit_comp
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3231 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rlimit.v')
-rw-r--r-- | theories/Reals/Rlimit.v | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 25b4ea7a6..dc849132f 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. (*********) |