diff options
author | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
commit | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch) | |
tree | fbb91e2f74c73bb867ab62c58f248a704bbe6dec /theories/Reals/RIneq.v | |
parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) |
Imported Upstream version 8.0pl3upstream/8.0pl3
Diffstat (limited to 'theories/Reals/RIneq.v')
-rw-r--r-- | theories/Reals/RIneq.v | 4 |
1 files changed, 2 insertions, 2 deletions
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). |