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/Ranalysis2.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/Ranalysis2.v')
| -rw-r--r-- | theories/Reals/Ranalysis2.v | 15 |
1 files changed, 6 insertions, 9 deletions
diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index 66bac9de7..1d44b3e73 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -51,11 +51,9 @@ Proof. apply prod_neq_R0; assumption. Qed. -Lemma Rmin_pos : forall x y:R, 0 < x -> 0 < y -> 0 < Rmin x y. -Proof. - intros; unfold Rmin in |- *. - case (Rle_dec x y); intro; assumption. -Qed. +(* begin hide *) +Notation Rmin_pos := Rmin_pos (only parsing). (* compat *) +(* end hide *) Lemma maj_term1 : forall (x h eps l1 alp_f2:R) (eps_f2 alp_f1d:posreal) @@ -386,10 +384,9 @@ Proof. apply Rplus_lt_compat_l; assumption. Qed. -Lemma Rmin_2 : forall a b c:R, a < b -> a < c -> a < Rmin b c. -Proof. - intros; unfold Rmin in |- *; case (Rle_dec b c); intro; assumption. -Qed. +(* begin hide *) +Notation Rmin_2 := Rmin_glb_lt (only parsing). +(* end hide *) Lemma quadruple : forall x:R, 4 * x = x + x + x + x. Proof. |