diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-27 08:31:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-27 08:31:45 +0000 |
| commit | 42331c8a1f29b97b6fa3300a667eea57deac86d0 (patch) | |
| tree | 994af72db1a54108fcab8f5607352f2a77f4ae34 /theories/Reals/DiscrR.v | |
| parent | 09db4999b6fd09dd33ccdd423f72b86d1eb9fe86 (diff) | |
Add a few properties about Rmin/Rmax with replication in Zmin/Zmax.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12358 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/DiscrR.v')
| -rw-r--r-- | theories/Reals/DiscrR.v | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v index 45e91577e..e037c77b5 100644 --- a/theories/Reals/DiscrR.v +++ b/theories/Reals/DiscrR.v @@ -16,14 +16,7 @@ Lemma Rlt_R0_R2 : 0 < 2. change 2 with (INR 2); apply lt_INR_0; apply lt_O_Sn. Qed. -Lemma Rplus_lt_pos : forall x y:R, 0 < x -> 0 < y -> 0 < x + y. -intros. -apply Rlt_trans with x. -assumption. -pattern x at 1 in |- *; rewrite <- Rplus_0_r. -apply Rplus_lt_compat_l. -assumption. -Qed. +Notation Rplus_lt_pos := Rplus_lt_0_compat (only parsing). Lemma IZR_eq : forall z1 z2:Z, z1 = z2 -> IZR z1 = IZR z2. intros; rewrite H; reflexivity. |