aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rseries.v
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-04-17 11:30:23 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-04-17 11:30:23 +0000
commitcc1be0bf512b421336e81099aa6906ca47e4257a (patch)
treec25fa8ed965729d7a85efa3b3292fdf7f442963d /theories/Reals/Rseries.v
parentebf9aa9f97ef0d49ed1b799c9213f78efad4fec7 (diff)
Uniformisation (Qed/Save et Implicits Arguments)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2650 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rseries.v')
-rw-r--r--theories/Reals/Rseries.v16
1 files changed, 8 insertions, 8 deletions
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.