From cc1be0bf512b421336e81099aa6906ca47e4257a Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 17 Apr 2002 11:30:23 +0000 Subject: Uniformisation (Qed/Save et Implicits Arguments) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/Rseries.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'theories/Reals/Rseries.v') diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index a388e2ae3..c88cdfaf2 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -49,18 +49,18 @@ Definition Un_growing:Prop:=(n:nat)(Rle (Un n) (Un (S n))). (*********) Lemma EUn_noempty:(ExT [r:R] (EUn r)). Unfold EUn;Split with (Un O);Split with O;Trivial. -Save. +Qed. (*********) Lemma Un_in_EUn:(n:nat)(EUn (Un n)). Intro;Unfold EUn;Split with n;Trivial. -Save. +Qed. (*********) Lemma Un_bound_imp:(x:R)((n:nat)(Rle (Un n) x))->(is_upper_bound EUn x). Intros;Unfold is_upper_bound;Intros;Unfold EUn in H0;Elim H0;Clear H0; Intros;Generalize (H x1);Intro;Rewrite <- H0 in H1;Trivial. -Save. +Qed. (*********) Lemma growing_prop:(n,m:nat)Un_growing->(ge n m)->(Rge (Un n) (Un m)). @@ -81,7 +81,7 @@ Unfold ge in H0;Generalize (H0 (S n0) H1 (lt_le_S n0 n1 y));Intro; Unfold Un_growing in H1; Apply (Rge_trans (Un (S n1)) (Un n1) (Un (S n0)) (Rle_sym1 (Un n1) (Un (S n1)) (H1 n1)) H3). -Save. +Qed. (* classical is needed: [not_all_not_ex] *) @@ -123,7 +123,7 @@ Intro;Elim (H6 N);Intro;Unfold Rle. Left;Unfold Rgt in H7;Assumption. Right;Auto. Apply (H1 (Un n) (Un_in_EUn n)). -Save. +Qed. (*********) Lemma finite_greater:(N:nat)(ExT [M:R] (n:nat)(le n N)->(Rle (Un n) M)). @@ -137,7 +137,7 @@ Rewrite <-H1;Rewrite <-H1 in H2; (eq_Rle (Un n) (Un n) (refl_eqT R (Un n))))). Apply (H2 (or_intror (Rle (Un n) (Un (S N))) (Rle (Un n) x) (H n H3))). -Save. +Qed. (*********) Lemma cauchy_bound:Cauchy_crit->(bound EUn). @@ -159,7 +159,7 @@ Unfold ge in H0;Generalize (H0 x2 (le_n x) y);Clear H0;Intro; Generalize (H2 x2 y);Clear H2 H0;Intro;Rewrite<-H in H0; Elim (Rmax_Rle x0 (Rplus (Un x) R1) x1);Intros;Clear H1;Apply H2; Left;Assumption. -Save. +Qed. End sequence. @@ -271,7 +271,7 @@ Assumption. Apply Rabsolu_pos_lt. Apply Rinv_neq_R0. Assumption. -Save. +Qed. -- cgit v1.2.3