Imported Upstream version 8.0pl3upstream/8.0pl3

4 files changed, 23 insertions, 18 deletions

diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v
index 13070bde..6087d3f2 100644
--- a/theories/Reals/PartSum.v
+++ b/theories/Reals/PartSum.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
  
-(*i $Id: PartSum.v,v 1.11.2.1 2004/07/16 19:31:11 herbelin Exp $ i*)
+(*i $Id: PartSum.v,v 1.11.2.2 2005/07/13 22:28:30 herbelin Exp $ i*)
 
 Require Import Rbase.
 Require Import Rfunctions.
@@ -489,8 +489,7 @@ elim s; intro.
 left; apply a.
 right; apply b.
 cut (Un_growing (fun n:nat => sum_f_R0 An n)).
-intro; set (l1 := sum_f_R0 An N).
-fold l1 in r.
+intro; set (l1 := sum_f_R0 An N) in r.
 unfold Un_cv in H; cut (0 < l1 - l).
 intro; elim (H _ H2); intros.
 set (N0 := max x N); cut (N0 >= x)%nat.
@@ -600,4 +599,4 @@ apply Rle_trans with (sum_f_R0 An n0 + Rabs (fn (S n0) x)).
 do 2 rewrite <- (Rplus_comm (Rabs (fn (S n0) x))).
 apply Rplus_le_compat_l; apply Hrecn0.
 apply Rplus_le_compat_l; apply H1.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index a23f53ff..5da14193 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: RIneq.v,v 1.23.2.1 2004/07/16 19:31:11 herbelin Exp $ i*)
+(*i $Id: RIneq.v,v 1.23.2.2 2005/03/29 15:35:13 herbelin Exp $ i*)
 
 (***************************************************************************)
 (**              Basic lemmas for the classical reals numbers              *)
@@ -1382,7 +1382,7 @@ Qed.
 
 (**********)
 Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
-intros z1 z2 H; apply Zlt_O_minus_lt. 
+intros z1 z2 H; apply Zlt_0_minus_lt. 
 apply lt_O_IZR.
 rewrite <- Z_R_minus.
 exact (Rgt_minus (IZR z2) (IZR z1) H).
diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v
index 51323ac4..ce33afdb 100644
--- a/theories/Reals/RiemannInt.v
+++ b/theories/Reals/RiemannInt.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
  
-(*i $Id: RiemannInt.v,v 1.18.2.1 2004/07/16 19:31:13 herbelin Exp $ i*)
+(*i $Id: RiemannInt.v,v 1.18.2.2 2005/07/13 23:18:52 herbelin Exp $ i*)
 
 Require Import Rfunctions.
 Require Import SeqSeries.
@@ -1593,13 +1593,12 @@ Lemma RiemannInt_P17 :
 intro f; intros; unfold RiemannInt in |- *;
  case (RiemannInt_exists pr1 RinvN RinvN_cv);
  case (RiemannInt_exists pr2 RinvN RinvN_cv); intros;
- set (phi1 := phi_sequence RinvN pr1);
+ set (phi1 := phi_sequence RinvN pr1) in u0;
  set (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N)));
  apply Rle_cv_lim with
   (fun N:nat => Rabs (RiemannInt_SF (phi1 N)))
   (fun N:nat => RiemannInt_SF (phi2 N)).
 intro; unfold phi2 in |- *; apply StepFun_P34; assumption.
-fold phi1 in u0;
  apply (continuity_seq Rabs (fun N:nat => RiemannInt_SF (phi1 N)) x0);
  try assumption.
 apply Rcontinuity_abs.
@@ -2372,10 +2371,11 @@ unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0;
  left; apply (cond_pos (RinvN n)).
 exists N0; intros; elim (H1 n); elim (H2 n); elim (H3 n); clear H1 H2 H3;
  intros; unfold R_dist in |- *; unfold Rminus in |- *; 
- rewrite Ropp_0; rewrite Rplus_0_r; set (phi1 := phi_sequence RinvN pr1 n);
- fold phi1 in H8; set (phi2 := phi_sequence RinvN pr2 n); 
- fold phi2 in H3; set (phi3 := phi_sequence RinvN pr3 n); 
- fold phi2 in H1; assert (H10 : IsStepFun phi3 a b).
+ rewrite Ropp_0; rewrite Rplus_0_r; 
+ set (phi1 := phi_sequence RinvN pr1 n) in H8 |- *;
+ set (phi2 := phi_sequence RinvN pr2 n) in H3 |- *; 
+ set (phi3 := phi_sequence RinvN pr3 n) in H1 |- *; 
+ assert (H10 : IsStepFun phi3 a b).
 apply StepFun_P44 with c.
 apply (pre phi3).
 split; assumption.
@@ -2442,7 +2442,7 @@ rewrite <- (Rabs_Ropp (f x - phi3 x)); rewrite Ropp_minus_distr;
  replace (phi3 x + -1 * phi2 x) with (phi3 x - f x + (f x - phi2 x));
  [ apply Rabs_triang | ring ].
 apply Rplus_le_compat.
-fold phi3 in H1; apply H1.
+apply H1.
 elim H14; intros; split.
 replace (Rmin a c) with a.
 apply Rle_trans with b; try assumption.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 55d4d958..27eb02cd 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -5,7 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(*i $Id: Zorder.v,v 1.6.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
+(*i $Id: Zorder.v,v 1.6.2.3 2005/03/29 15:35:12 herbelin Exp $ i*)
 
 (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
@@ -849,12 +849,15 @@ intros p H1; unfold Zgt in |- *; pattern 0 at 2 in |- *;
 intros p H; discriminate H.
 Qed.
 
-Lemma Zmult_lt_O_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m.
+Lemma Zmult_lt_0_compat : forall n m:Z, 0 < n -> 0 < m -> 0 < n * m.
 intros a b apos bpos.
 apply Zgt_lt.
 apply Zmult_gt_0_compat; try apply Zlt_gt; assumption.
 Qed.
 
+(* For compatibility *)
+Notation Zmult_lt_O_compat := Zmult_lt_0_compat (only parsing).
+
 Lemma Zmult_gt_0_le_0_compat : forall n m:Z, n > 0 -> 0 <= m -> 0 <= m * n.
 Proof.
 intros x y H1 H2; apply Zmult_le_0_compat; trivial.
@@ -958,8 +961,11 @@ intros n m H; apply Zplus_lt_reg_l with (p := m); rewrite Zplus_minus;
  assumption.
 Qed.
 
-Lemma Zlt_O_minus_lt : forall n m:Z, 0 < n - m -> m < n.
+Lemma Zlt_0_minus_lt : forall n m:Z, 0 < n - m -> m < n.
 Proof.
 intros n m H; apply Zplus_lt_reg_l with (p := - m); rewrite Zplus_opp_l;
  rewrite Zplus_comm; exact H.
-Qed.
\ No newline at end of file
+Qed.
+
+(* For compatibility *)
+Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).