diff options
| author |  Yves Bertot <bertot@inria.fr> | 2014-09-23 13:11:24 +0200 |
|---|---|---|
| committer | Yves Bertot <bertot@inria.fr> | 2014-09-23 13:11:24 +0200 |
| commit | 13ab2df9ed3a5ea6b7455ea8a7da4341e7f2bcd5 (patch) | |
| tree | fd42f041d099700403dfc0a3af69ea5791ec5930 /theories/Reals/Rtopology.v | |
| parent | 85355cfda7a01fa532f111ee7c4d522a8be8a399 (diff) | |
adds general facts in the Reals library, whose need was detected in
experiments about computing PI
Diffstat (limited to 'theories/Reals/Rtopology.v')
| -rw-r--r-- | theories/Reals/Rtopology.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index ac15cf21e..e9423de6f 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -965,12 +965,6 @@ Proof. intros; exists (f0 x0); apply H4. Qed. -Lemma Rlt_Rminus : forall a b:R, a < b -> 0 < b - a. -Proof. - intros; apply Rplus_lt_reg_l with a; rewrite Rplus_0_r; - replace (a + (b - a)) with b; [ assumption | ring ]. -Qed. - Lemma prolongement_C0 : forall (f:R -> R) (a b:R), a <= b -> |