diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Reals/PartSum.v | 7 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 4 | ||||
| -rw-r--r-- | theories/Reals/RiemannInt.v | 16 | ||||
| -rw-r--r-- | theories/ZArith/Zorder.v | 14 |
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). |